50 years of proof assistants
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 mythical conference on Proving and Improving Programs held at Arc-et-Senans. The user manual, published in the Springer lecture notes series, came out in 1979. Edinburgh LCF introduced some other principles that people still adhere to today:
inference rules in the natural deduction style, with a dynamic set of assumptions
a goal-directed proof style, where you start with the theorem statement and work backwards
a structured system of theories to organise groups of definitions
Edinburgh LCF had its own version of the ML language. It supported a fragment of first-order logic containing the logical symbols $\forall$, $\land$ and $\to$ along with the relation symbols $\equiv$ and $\sqsubseteq$. It introduced proof tactics and also tacticals: operators for combining tactics. Tactics supported goal-directed proof, but Edinburgh LCF had no notion of the current goal or anything to help the user manage the tree of subgoals. Its user interface was simply the ML top level and the various theorem-proving primitives were simply ML functions. ML stood for metalanguage, since managing the process of proof was its exact job.
... continue reading