“Correctness of a compiler for arithmetic expressions” (McCarthy and Painter 1967) describes the first proof of compiler correctness. To make it easier to play with the proof, I coded it up using the Lean theorem prover.

The Lean code is self-explanatory, so I won’t go into the details here.

Lean’s support for calculational proofs is particularly nice for mirroring the proof in the paper. For example, below is an excerpt of the proof in the paper:

\[\begin{aligned} \zeta_1 & = \mathit{outcome}(\mathit{compile}(s1(e),t),\eta) \\ & =_t a(\mathit{ac}, \upsilon_1, \eta) & \textrm{Induction Hypothesis} \end{aligned}\]

Here’s the corresponding part in Lean:

calc ζ₁
    = outcome (compile map e_s₁ t) η : by cc
... ≃[t] {ac := ν₁, ..η}             : by apply e_ih_s₁; assumption


The reprint version of the paper contains a number of typos (not present in the original version):

  • Theorem 1: “\(c(\mathit{loc}(v, \eta) = c(v, \xi)\)” should be “\(c(\mathit{loc}(v, \mathit{map}), \eta) = c(v, \xi)\).”

  • Section 5.III, under “\(\zeta_2 = \mathit{outcome}(\mathit{mksto}(t), \zeta_1)\)”: “\(a(t, \upsilon_1), \zeta_1)\)” should be “\(a(t, \upsilon_1, \zeta_1)\).”

  • Section 5.III, next to “\(c(\mathit{loc}(\upsilon, \mathit{map}), \zeta_2)\)”: “\(c(\mathit{loc}(\upsilon), \mathit{map})a(t, \upsilon_1, \eta))\)” should be “\(c(\mathit{loc}(\upsilon, \mathit{map}), a(t, \upsilon_1, \eta))\).”