Proof, Models and Mathematics
A short history of formal methods, from Turing's checked routine to Lean 4, read against the limits of verification
Table of Contents
Overview
'bounds explain why the strands diverged' is unsourced causation; reworded as the note's reading
Formal methods is three histories that share a vocabulary: proving that a program meets its specification, checking a model of a system against a property, and writing mathematics so that a machine can check every step. Each began with a paper that still reads well, each became practical decades later, and each is still bounded by the same results about what computation can decide.
This note dates the main steps in each strand and cites the source for each, then sets them against those bounds. The bounds come first; this note reads each strand as a way of living within them.
The site's working notes on the tools mentioned here: Alloy, TLA+ in a build pipeline, Lean 4 on FreeBSD, a Lean parity proof, Dafny and Clojure and the tools of Logic for Programmers.
The limits
All 6 keys resolve and match Crossref/source; turing1936 year 1937->1936 in bib (parts appeared Nov/Dec 1936; 1937 is the volume year); yuan2014 gained publisher/ISBN/URL; prose unchanged
| claim-validator: Pressler summary holds; Goedel misattributed to decidability; 'exponential in components' not in Pressler; decomposition = Demri et al. 2005 non-FPT; Yuan is 92% mishandled errors, 58% caught by simple tests, not all
Ron Pressler's 2016 essay, "Why Writing Correct Software Is Hard", collects the results that bound every method below (Pressler 2016). Its argument, briefly: the difficulty of correct software is in the foundations of computation, not in poor tools.
- Undecidability. Gödel's incompleteness theorems (Gödel 1931) end the hope of a complete, provably consistent foundation; Turing's halting result (Turing 1936) ends the hope of a general procedure for deciding whether a program terminates. Rice's theorem extends this to every non-trivial semantic property of programs (Rice 1953).
- Complexity. Even where a question is decidable, it can be intractable. A proof system with short proofs of every tautology exists if and only if NP = coNP (Cook and Reckhow 1979). Model checking is linear in the size of the state space, with a factor linear in the formula for CTL and exponential in it for LTL; the trouble is the state space, which even a small program makes huge, and symbolic model checking is PSPACE-complete.
- No free decomposition. Pressler cites Demri, Laroussinie and Schnoebelen (2005): verifying a system of k components is probably not fixed-parameter tractable in k, so splitting it into modules does not, in general, make verification cheaper.
His conclusion is that correctness comes at a significant cost, and that what helps is empirical study of real programs and partial techniques: local properties, heuristics, approximations. One study he cites found that 92% of catastrophic failures in distributed data systems came from mishandled non-fatal errors, and that in 58% simple tests of the error-handling code would have exposed the fault (Yuan et al. 2014).
This note reads each strand below as a different way of paying that cost: with human effort (proof), by limiting what is checked (models), or by working only in mathematics, where the statements are fixed and the proofs are worth the labour.
Proving programs
All 8 keys match Crossref; turing1949 (no DOI) matches Turing Archive AMT/B/8: conference 24 June 1949, Report pp. 67-69; prose unchanged
| claim-validator: Hoare 1969 writes P {Q} R; CoC is Coq's origin, CIC its basis; Coq/Lean use de Bruijn proof-term checking, not LCF's abstract type (Paulson 2022)
| year | step | source |
|---|---|---|
| 1949 | Turing's "Checking a Large Routine": a program annotated with assertions about its state, and an argument that it terminates | (Turing 1949) |
| 1967 | Floyd: assertions attached to the edges of a flowchart give a program its meaning, and verification conditions follow from them | (Floyd 1967) |
| 1969 | Hoare: the triple, written P {Q} R in the paper (now {P} Q {R}), and an axiomatic system for reasoning about programs | (Hoare 1969) |
| 1975 | Dijkstra: guarded commands and the weakest precondition, which turn verification into a calculus for deriving programs | (Dijkstra 1975) |
| 1979 | Edinburgh LCF: a theorem prover whose theorems can be built only by a small kernel of inference rules, an abstract type in ML | (Gordon, Milner, and Wadsworth 1979) |
| 1988 | The Calculus of Constructions, the type theory Coq first implemented, later extended with inductive types (Coq history) | (Coquand and Huet 1988) |
| 2009 | CompCert: a C compiler proved in Coq to preserve the meaning of the programs it compiles | (Leroy 2009) |
| 2009 | seL4: an operating-system microkernel with a machine-checked proof that its C implementation refines its specification | (Klein et al. 2009) |
LCF's idea lasted: whatever automation searches for a proof, only a small kernel can produce a theorem, so the trust rests on a small piece of code. HOL and Isabelle keep LCF's abstract type; Coq and Lean reach the same end differently, by rechecking proof terms, the de Bruijn criterion (Paulson on the two designs).
Checking models
All 6 keys match Crossref; clarke1981 year 1982 is correct (1981 workshop, LNCS 131 published 1982), editor Kozen and workshop note added; prose unchanged
| claim-validator: Rows hold against sources; Clarke-Emerson 1981 workshop/1982 LNCS, Queille-Sifakis independent; Newcombe reports serious bugs found pre-production
| year | step | source |
|---|---|---|
| 1977 | Pnueli: temporal logic as a language for the properties of programs that run forever | (Pnueli 1977) |
| 1981 | Clarke and Emerson: branching-time temporal logic checked mechanically against a finite model | (Clarke and Emerson 1982) |
| 1982 | Queille and Sifakis, independently: model checking in the CESAR system | (Queille and Sifakis 1982) |
| 1994 | Lamport: the Temporal Logic of Actions, the basis of TLA+ | (Lamport 1994) |
| 2002 | Jackson: Alloy, a lightweight relational modelling language checked within bounds | (Jackson 2002) |
| 2015 | Amazon Web Services reports using TLA+ on production designs and finding serious bugs before release | (Newcombe et al. 2015) |
Model checking pays the cost by checking a model rather than the program, and a bounded or finite one. Alloy makes the bound explicit (a scope); TLC explores the reachable states of a TLA+ specification. What it gives in exchange is automation: no proof to write, and a counterexample when the property fails.
Formalising mathematics
Bib fields verified (castelvecchi2021 issue 7865 added); prose: Mizar began 1973 at Plock, moved to Bialystok 1976; Gonthier 2005 report is sole-authored, Notices PDF 403 so Werner credit unverified at primary; prose unchanged
| claim-validator: Mizar began at Plock 1973, Bialystok 1976, 'one of the largest' unsupported by cited source; LTE 2021 completed Theorem 9.4 only (Scholze: about half-way); Werner credit per MSR blog
| editor 2026-11-13: both disputes resolved; Mizar corrected by claim-validator (Płock 1973, Białystok 1976); Werner dropped, since the cited article is by Gonthier alone and no primary source confirming Werner could be opened
| year | step | source |
|---|---|---|
| 1968 | de Bruijn's Automath: a language in which mathematics can be written and its proofs checked by machine | (de Bruijn 1970) |
| 1973 | Mizar begins under Andrzej Trybulec, at Płock and from 1976 at Białystok; its Mizar Mathematical Library collects formalised definitions and theorems | (Grabowski, Korniłowicz, and Naumowicz 2010) |
| 2005 | Gonthier: the Four Colour Theorem formalised in Coq | (Gonthier 2008) |
| 2014 | Flyspeck: a formal proof of the Kepler conjecture, in HOL Light and Isabelle | (Hales and others 2017) |
| 2015 | The Lean theorem prover, from Microsoft Research | (de Moura et al. 2015) |
| 2020 | mathlib, Lean's community library of mathematics | (The mathlib Community 2020) |
| 2021 | Lean 4, a theorem prover that is also a programming language, its system largely written in Lean | (de Moura and Ullrich 2021) |
| 2021 | The Liquid Tensor Experiment: the key step (Theorem 9.4) of a central theorem of Clausen and Scholze's condensed mathematics checked in Lean (Scholze, June 2021) | (Castelvecchi 2021) |
The site's Lean notes run Lean 4 and mathlib on FreeBSD and check one small proof against its generated code: Lean 4 on FreeBSD 15 and the parity proof.
The limits, again
Section is the note's framing, now marked; dropped unsupported causal claim that formalised maths became practical first because statements are fixed
None of the three strands escapes the results in the limits. On this note's reading, each chooses where to pay.
- Proof pays with human effort. The kernel checks every step, but a person (or a search) has to find the steps, and the specification has to be the right one. CompCert and seL4 are the evidence that the cost can be paid for systems that matter.
- Model checking pays by checking less: a model rather than the code, within a bound, with the state space as the constraint. It finds bugs in designs cheaply and proves nothing outside its bound.
- Formalised mathematics pays where the statement is fixed and the proof is worth more than the labour.
Testing sits outside all three and pays in its own currency: it runs the program, so it sees only the runs it makes. The lab notes on this site measure that directly, with reach counts and planted faults: Harness first.