From 4353f331b5ab4af157f576f54b1cc79dd08abb12 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 23 Apr 2025 15:59:22 +0100
Subject: Current state of affairs.

---
 sec/compiler.ltx | 25 +++++++++++++++++++------
 1 file changed, 19 insertions(+), 6 deletions(-)

(limited to 'sec/compiler.ltx')

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}
 }
 
-- 
cgit v1.2.3

