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 , either is a value, or there exists such that evaluates to in one step. Formally, .
Theorem (Totality): For any expression , there exists such that is a value and evaluates to in zero or more steps. Formally, .
Theorem (Preservation): If is a natural number in the initial type environment, and evaluates to in one step, then is a natural number in the initial type environment. Formally, .
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 constructions1, with a countable hierarchy2 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-check3, letting you use fib
in the rest of your program as
if it were implemented correctly.
Footnotes
- This type theory is also the basis of other proof assistants, such as Coq. ↩
- The type theory utilizes a hierarchy of such universes in order to avoid Girard's paradox, the type-theoretical equivalent of Russell's paradox. ↩
- Interestingly, this exposes a deficiency of OCaml as it exists today, which
is that it doesn't support algebraic effects. If it did, the function signature
may encode the fact that it throws an exception (e.g. using some imaginary
syntax,
int -> int exn
), which is different from the desired signature. ↩