Include cautionary tale.

1 files changed, 13 insertions, 6 deletions

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index cfb5be5..89a5ffb 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -239,12 +239,19 @@ synths : (tm : Term context) -> (env : TyEnv context) -> Maybe (a : Ty ** Synths
 The result explicitly depends on the input invalidating the trivial
 implementation.
 
-\TODO{
-  \begin{itemize}
-    \item describe why knowing there is a derivation is necessary
-    \item explain why these extra features do not guarantee compiler correctness
-  \end{itemize}
-}
+\TODO{describe why knowing there is a derivation is necessary}
+
+We want to emphasise that producing a certificate during type checking
+does not prove the type checker is correct. The certificate only
+proves the type checker matches the specification, which may be
+wrong. As a concrete example, the initial Idris~2 specification for
+\lang{} certificates had a bug. When checking an abstraction with
+multiple arguments, the types were assigned to variables in reverse
+order. For instance when checking \verb|\x, y => x| at type \(A \to B \to
+A\), the specification assigned \verb|x| type \(B\) and \verb|y| type
+\(A\). Thus, the certified type checker followed the specification and
+rejected this term, and even produced a certificate of why it was
+right to do so.
 
 \subsection{Scheme Backend}
 \TODO{