For my final project in CS242, I used the Lean theorem prover to prove type safety for a small, toy language.

In order to prove type safety, I proved three distinct properties:

Theorem (Progress): For any expression $e$, either $e$ is a value, or there exists $e'$ such that $e$ evaluates to $e'$ in one step. Formally, $\forall e \in \mathcal{E}. e \textbf{ val} \vee (\exists e' \in \mathcal{E}. e \mapsto e')$.

Theorem (Totality): For any expression $e$, there exists $e'$ such that $e'$ is a value and $e$ evaluates to $e'$ in zero or more steps. Formally, $\forall e \in \mathcal{E}. \exists e' \in \mathcal{E}. e' \textbf{ val} \wedge e \mapsto^* e'$.

Theorem (Preservation): If $e$ is a natural number in the initial type environment, and $e$ evaluates to $e'$ in one step, then $e'$ is a natural number in the initial type environment. Formally, $\forall e, e' \in \mathcal{E}. 0 \vdash e : \textbf{ nat} \wedge e \mapsto e' \rightarrow 0 \vdash e' : \textbf{ nat}$.

Lean's type system is more advanced than that of any other language I have used. It is based on a version of dependent type theory known as the calculus of constructions¹, with a countable hierarchy² of non-cumulative universes and inductive types. This powerful type system provides the necessary power and expressivity to formalize proofs about complex systems within the language.

Although there are many ways to write proofs in Lean, I mostly used tactics. As described in the documentation, tactics "support an incremental style of writing proofs, in which users decompose a proof and work on goals one step at a time".

There's a special tactic called sorry, which automatically satisfies the relevant goal in scope, though it also displays a warning at the enclosing theorem or lemma, since the proof is technically incomplete. This led to a very pleasant programming experience, since I was able to stub out the complicated parts of the proof with sorry, work on the easier bits, and then revisit the harder ones once I was confident that the proof structure was sound. In fact, we often do this in programming. In OCaml, for example, you can stub out a function as follows:

let fib (x : int) : int = raise_s [%message "Not implemented!"]

This will type-check³, letting you use fib in the rest of your program as if it were implemented correctly.

Footnotes