Justify extrinsic certificate.

1 files changed, 20 insertions, 3 deletions

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index decb2af..cfb5be5 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -219,11 +219,28 @@ have not done this. Our more lax certificates are still sufficiently
 expressive to prove a term cannot have both a positive and negative
 certificate.
 
+\TODO{explain the derivation is runtime erased}
+
+Like with the well-scoped AST, we have the choice for type checking to
+produce an intrisically well-typed AST.\@ We have opted against it
+because it is harder to express the relation between the input and
+output terms. Consider the hypothetical signature of the type
+synthesis function for an intrinsically well-typed AST:
+\begin{verbatim}
+synths : Term context -> (env : TyEnv context) -> Maybe (a : Ty ** WfTerm env a)
+\end{verbatim}
+The result does not depend on the given input term, so we can give a
+trivial implementation such as the function constantly returning a
+well-typed closed term. Compare this to a (simplified) signature for
+synthesis with an extrinsic certificate:
+\begin{verbatim}
+synths : (tm : Term context) -> (env : TyEnv context) -> Maybe (a : Ty ** SynthsTy env tm a)
+\end{verbatim}
+The result explicitly depends on the input invalidating the trivial
+implementation.
+
 \TODO{
   \begin{itemize}
-    \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}