Current state of affairs.

1 files changed, 19 insertions, 6 deletions

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index dde2856..2cfde8e 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -6,12 +6,25 @@
 
 \TODO{
   \begin{itemize}
-    \item QTT basics
-    \item intrinsically well-scoped AST
-    \item bidirectional judgement
-    \item well-typed data types
-    \item type checking function
-    \item irrelevant pattern matching
+    \item describe that I have a type checker and compiler implemented in Idris
+    \item explain what intentionally well-scoped syntax is
+    \item justify why I used intentionally well-scoped syntax
+    \item describe how type checking produces a derivation
+    \item explain the derivation is runtime erased
+    \item justify the derivation having no runtime cost
+    \item describe why knowing there is a derivation is necessary
+    \item explain why these extra features do not guarantee compiler correctness
+  \end{itemize}
+}
+
+\TODO{
+  \begin{itemize}
+    \item justify how dynamic types make Scheme a good compilation target
+    \item describe how products are compiled to assoc-lists
+    \item describe how sums are compiled to tagged values
+    \item describe how dynamic typing removes the need for roll
+    \item explain why fold needs to know the term has a valid type
+    \item explain why fold must be compiled recursively with map
   \end{itemize}
 }