LCF: a program that checks proofs about computation
In May 1972 Robin Milner described LCF in a Stanford Artificial Intelligence Project memo: a program that checks formal proofs in the logic of computable functions that Dana Scott had proposed at Oxford in the autumn of 1969. A person states a goal and splits it into subgoals; the machine carries the proof and checks each step.
Why it matters
Proof became a dialogue: the person decides where to go, the machine guarantees that each step is sound. In the Edinburgh version this dialogue got a language of its own, ML; Gordon, who worked on the project, writes that the descendants of LCF form a whole paradigm of computer-assisted reasoning.
The memo presents Scott's logic in the notation of the typed lambda calculus and the machine implementation of a proof checker for it; its commands include a separate group for stating goals and working on subgoals interactively. NASA and ARPA supported the work. The memo gives no figures. Edinburgh LCF is described here from the book of 1979 itself (Gordon, Milner and Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, Lecture Notes in Computer Science 78), of which the preface and the first two pages of the introduction are open, and from a retrospective by Mike Gordon. By the preface, the fixed commands of Stanford LCF made for long and repetitive interactions, so the new system replaced them with a general-purpose programming language, ML (for metalanguage): higher-order, with exception handling and a secure polymorphic type discipline. Theorems are computed values of the type thm, and the type system guarantees that every value of that type is a theorem, since only inference rules can compute one. The introduction calls the small building blocks of proof strategies tactics and the operations that combine them tacticals, and says ML was designed to make both easy to program. The system ran on a DECsystem-10. The authors write that Lockwood Morris and Malcolm Newey should have been co-authors had it been feasible. Gordon adds that Milner moved to Edinburgh around 1973. The book gives no date for the start of the Edinburgh work; its introduction dates the Stanford implementation to 1971-2. Avra Cohn, who took part in the final design stages, wrote in her Edinburgh thesis of 1979 that the system was implemented in 1974-1979 by Gordon, Milner, Morris, Newey and Wadsworth. What the record does not claim: anything from the chapters of the book beyond the preface and the opening of the introduction, which are paywalled. The preface speaks of a secure type discipline; that theorems form an abstract type is Gordon's wording.