From 19fa9faa7e56d9ace846e92aeee2085d6ab4cf2d Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 12 Jun 2025 17:44:00 +0100 Subject: Include cautionary tale. --- sec/compiler.ltx | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'sec') 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{ -- cgit v1.2.3