LCF and the tactic idea

LCF was a proof checker built by Robin Milner, first at Stanford in 1972 and then, in a new design, at Edinburgh. Two ideas from the Edinburgh design run through many proof assistants since: a protected type of theorems, so that only the rules of the logic can produce one, and tactics, programs that reduce a goal to simpler goals. To make tactics programmable, Milner and his colleagues designed a programming language, ML. This page follows those ideas from 1972 to Lean.

Stanford LCF

"LCF" stands for Logic for Computable Functions, Milner's name for a logic Dana Scott devised in 1969 for reasoning about recursively defined functions; Scott's manuscript was not published until 1993. Milner built the first checker for it at Stanford in 1972, with Whitfield Diffie, Richard Weyhrauch and Malcolm Newey. His report of that year describes it as an interactive program for generating formal proofs about computable functions, helped by a subgoaling facility and a simplifier.

A user stated a goal and split it into subgoals with a fixed set of commands, such as induction, until the simplifier could finish each one. Gordon names two limits of the system. The proofs it stored filled the available memory, and its fixed set of proof commands could not easily be extended.

Edinburgh LCF and the type of theorems

Around 1973 Milner moved to Edinburgh and began a successor, Edinburgh LCF, first with Lockwood Morris and Malcolm Newey, and from 1975 with Christopher Wadsworth and Mike Gordon.

The answer to the first limit was to keep theorems and discard proofs. To keep that safe, Milner made theorem an abstract data type. Its only given values were instances of the axioms, and its only operations were the rules of inference. A program could hold a value of type theorem only if it had obtained it from axioms by applying rules, so type checking alone guaranteed that every such value was a theorem of the logic. The steps of a proof were carried out but not recorded. The guarantee lies in the programming language, not in a stored proof that someone else could check later.

ML, tactics and tacticals

The answer to the second limit was a programming language in which users could write their own proof procedures. Milner, with Morris and Newey, designed ML, the "Meta Language", strictly typed so that the abstract type of theorems could not be circumvented. It was described at the 1978 Symposium on Principles of Programming Languages. Milner's account of ML's polymorphic type inference appeared the same year.

In ML a strategy for reducing a goal to subgoals is a function, which Milner called a tactic. Operations that combine strategies, taking tactics as arguments and returning tactics, are higher-order functions, which he called tacticals. Since a tactic may be applied to a goal it cannot handle, ML was given exceptions, so that a failing tactic could signal failure and another be tried. Gordon records that the needs of theorem proving shaped the first ML in detail.

The work was written up as Edinburgh LCF by Gordon, Milner and Wadsworth in 1979. In 1991 Milner received the ACM Turing Award; the citation names LCF, "probably the first theoretically based yet practical tool for machine-assisted proof construction", and ML among his achievements.

Descendants

Cambridge LCF. In the early 1980s Lawrence Paulson at Cambridge and Gérard Huet in France reworked the system together. Huet improved and extended ML, and his group went on to develop Caml. Paulson's version, Cambridge LCF, was completed around 1985 and described in his 1987 book Logic and Computation.

HOL. Gordon adapted Cambridge LCF to classical higher-order logic for verifying hardware. HOL kept LCF's syntax, its abstract type of theorems and its tactics, but read types as ordinary sets. A stable version, HOL88, appeared in about 1988. Reimplementations followed: HOL90, in Standard ML, by Konrad Slind, and HOL Light, in Caml Light, by John Harrison and Konrad Slind. In 2017 Ebner and colleagues noted that HOL4 and HOL Light still work in the original LCF manner, with the user interacting directly in ML.

Isabelle. Paulson then built Isabelle, a generic prover in which the rules of many logics are stated declaratively in a common metalogic and combined by higher-order unification. Gordon notes that Isabelle keeps Milner's key idea, the abstract type of theorems, and lifts it to the metalogic.

Type theories. The LCF method, with ML as its metalanguage, was also applied to logics quite unlike Scott's. Gordon lists Nuprl, a proof system for Martin-Löf type theory, and one for the Calculus of Constructions among the LCF-style systems. Those are the subjects of Martin-Löf type theory and The Calculus of Constructions.

The line to Lean

Lean took the tactic idea and changed where the guarantee lies. In Lean, as in Automath, a proof is a term of the type that states the theorem. Tactics are instructions that describe how to construct such a term, and they support writing a proof incrementally, one step at a time. The first description of Lean, in 2015, presents tactics as one way, beside writing terms directly, of constructing proof terms, as in Coq, HOL Light, Isabelle and PVS, and describes Lean's small trusted kernel and proof terms that can be checked independently. In LCF a faulty tactic is stopped by the type discipline of ML; in Lean whatever term a tactic produces must still pass Lean's kernel. The two arrangements are compared at What has to be trusted.

Lean also took the metalanguage idea, but made the metalanguage Lean itself. The 2017 paper on Lean 3's metaprogramming framework recalls that ML was designed as the metalanguage for LCF, and describes tactics written in Lean, in the same files and with the same library as the mathematics they serve. Lean 4 goes further: it is implemented largely in Lean, and users can extend its parser, elaborator and tactics in Lean. How tactics work in Lean today is described at Tactics and The tactic framework.

Provenance: Gordon's 2000 history, the Lean papers of 2015, 2017 and 2021 and the tactics chapter of Theorem Proving in Lean 4 were read for this page. Milner's 1972 report was read in its opening pages only. Milner's 1978 paper was read in its opening pages, and Paulson's 1989 paper in its preprint (abstract and history). The 1978 POPL paper and the 1979 book were not opened; their details come from Gordon's reference list and the publishers' records. The account of Stanford and Edinburgh LCF follows Gordon, a participant from 1975.

Next

Martin-Löf type theory