50 years of proof assistants

Summary

50 years of proof assistants 05 Dec 2025 [ memories LCF HOL system Isabelle Coq MJC Gordon ] Crackpots ranging from billionaire Peter Thiel to random YouTube influencers claim that science has been stagnating for the past 50 years. They admit that computing is an exception: they don’t pretend that my personal 32GB laptop is not an advance over the 16MB mainframe that served the whole Caltech community when I was there. Instead they claim that advances in computing were driven solely by industrial research, quite overlooking the role of academia and government funding in pushing the VLSI revolution, RISC processor design, networking, hypertext, virtual memory and indeed computers themselves. As for the industrial research, most of it came from just two “blue sky” institutes – Bell Labs and Xerox PARC – that closed a long time ago. LCF-style proof assistants are a world away from mainstream computing, so let’s look at 50 years of progress there. 1975–1985: Edinburgh LCF The first instance of LCF was Stanford LCF, developed by Robin Milner in 1972, but it was not an LCF-style proof assistant! LCF meant “Logic for Computable Functions”, a quirky formalism based on Scott domains and intended for reasoning about small functional programs. But “LCF-style proof assistant” means one that, like Edinburgh LCF, was coded in some form of the ML programming language and provided a proof kernel, encapsulated in an abstract type definition, to ensure that a theorem could only be generated by applying inference rules to axioms or other theorems: … the ML type discipline is used… so that—whatever complex procedures are defined—all values of type thm must be theorems, as only inferences can compute such values…. This security releases us from the need to preserve whole proofs… — an important practical gain since large proofs tended to clog up the working space… [Edinburgh LCF, page IV] Edinburgh LCF was first announced in 1975, which conveniently is exactly 50 years ago, at the almost...