From 8c2d503f85533c4070e7832ec82198f52d7d125e Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 30 May 2025 14:53:50 +0100
Subject: Reorder and extend TODOs.

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

(limited to 'sec/compiler.ltx')

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index b4fde16..0948073 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -17,28 +17,36 @@ three main components:
 
   \item Second we perform type checking using a bidirectional
     algorithm~\cite{bidir}. Along with the usual type checking result,
-    the algorithm produces a runtime-erased proof that the term is
-    well-typed.
+    the algorithm produces a runtime-erased typing derivation.
 
   \item Finally we compile the term to Guile~Scheme~\cite{guile}. By
-    requiring an erased well-typedness proof, the compiler can
-    statically guarantee it will only ever have to process well-typed
-    terms.
+    requiring an erased type derivation, the compiler can statically
+    guarantee it will only ever have to process well-typed terms.
 \end{itemize}
 
-
+\subsection{Parser}
 \TODO{
   \begin{itemize}
+    \item summarise \textcite{bidir}
+    \item explain dependent state
     \item explain what intentionally well-scoped syntax is
     \item justify why I used intentionally well-scoped syntax
+  \end{itemize}
+}
+
+\subsection{Bidirectional Type Checker}
+\TODO{
+  \begin{itemize}
     \item describe how type checking produces a derivation
     \item explain the derivation is runtime erased
+    \item justify extrinsic derivation
     \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}
 }
 
+\subsection{Scheme Backend}
 \TODO{
   \begin{itemize}
     \item justify how dynamic types make Scheme a good compilation target
-- 
cgit v1.2.3

