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. For Edinburgh LCF the record rests not on the 1979 book, which could not be read, but on a retrospective by Mike Gordon, who worked on it: around 1973 Milner moved to Edinburgh; so that a theorem could be obtained only by proof, theorems were made values of an abstract type whose operations are the inference rules; for this Milner, with Morris and Newey, designed the strictly typed language ML (Meta Language), and proof strategies became functions that Milner called tactics. What the record does not claim: dates or contents of the 1979 book beyond what Gordon says.