diff --git a/icfp-2016/correctness.scrbl b/icfp-2016/correctness.scrbl
deleted file mode 100644
index 48b737a..0000000
--- a/icfp-2016/correctness.scrbl
+++ /dev/null
@@ -1,14 +0,0 @@
-@title{Correctness}
-
-Our implementation of @racket[format] in @todo{figure-ref} exhibits a few desirable properties.
-@itemlist[
-  @item{}
-]
-
-Generally speaking these properties are the ``right'' way to judge if a transformation is correct.
-
-
-
-Open question: can we design a restricted macro language where every transformation
- is statically checked to ensure termination and correctness.
-
diff --git a/icfp-2016/implementation.scrbl b/icfp-2016/implementation.scrbl
index 0248d59..f8b7683 100644
--- a/icfp-2016/implementation.scrbl
+++ b/icfp-2016/implementation.scrbl
@@ -13,3 +13,25 @@
 @; We don't re-implement format or regexp,
 @; but we do implement + and some vector operations, to go faster
 
+
+
+
+
+
+@section{Correctness}
+
+Our implementation of @racket[format] in @todo{figure-ref} exhibits a few desirable properties.
+@itemlist[
+  @item{}
+]
+
+Generally speaking these properties are the ``right'' way to judge if a transformation is correct.
+
+
+
+Open question: can we design a restricted macro language where every transformation
+ is statically checked to ensure termination and correctness.
+
+We have argued that our macros help typed programming, but they did so only
+ by going outside the law of the type checker.
+