Summary

  • Edinburgh LCF let programmable tactics search backward from a goal, but a successful search still had to return through a validation composed from protected inference rules. A tactic could fail or be wrong without acquiring a second way to manufacture a theorem value.
  • The theorem abstract type reduced the code directly trusted for theorem construction. It did not prove the consistency of the chosen logic, the fidelity of a specification, or the correctness of the compiler, runtime and hardware beneath the abstraction.
  • The history is collaborative: Dana Scott supplied the underlying logic; Stanford LCF preceded Edinburgh LCF; Michael Gordon, Christopher Wadsworth, Lockwood Morris, Malcolm Newey and a wider community helped build the system and its metalanguage. Later provers inherited and changed the idea rather than sharing one identical architecture.

The last step is different from all the steps before it

Imagine an automated tactic expanding a goal into subgoals, trying rewrites, backtracking and combining strategies. Its trace may be long and persuasive. It may even end with a message that all branches have been discharged. Yet none of those events, by themselves, qualifies the result as a theorem in the LCF sense.

The crossing occurs later. The tactic returns a validation: a function that expects theorem values for the proposed subgoals and uses them to produce a theorem for the original goal. When the subgoals have been proved, that validation performs forward inference through the protected theorem interface. If it cannot do so, the search has not earned acceptance, however attractive its transcript looks.

This distinction was a practical answer to a hard design problem. An interactive prover must be extensible enough for users to express new proof methods. Those methods can be complex, experimental and erroneous. But giving every new procedure unrestricted authority to create a theorem would enlarge the trusted surface with every extension. LCF instead placed theorem construction behind an abstract type, conventionally named thm. Axioms and primitive inference rules were the operations able to return values of that type.

The architecture did not make tactics correct. A tactic can choose unsuitable subgoals, diverge, raise an exception or provide a validation that does not deliver the promised conclusion. Larry Paulson's retrospective description is explicit about that possibility. The important negative power is narrower: ordinary code does not gain an alternative constructor merely because its search procedure is sophisticated. Error normally becomes failure to obtain the requested theorem, not permission to mint one.

From a proof checker to a programmable prover

Milner's 1972 account described an implemented proof checker for Dana Scott's Logic for Computable Functions. That Stanford work established the setting, but long proofs exposed severe costs. Low-level checking was tedious, while retaining full proof histories strained the machines available at the time. After Milner moved to Edinburgh in 1973, the project developed a more programmable environment.

The canonical history is not a lone-inventor narrative. The 1979 book Edinburgh LCF is by Michael J. C. Gordon, Robin Milner and Christopher P. Wadsworth. The 1978 paper on the metalanguage also names Lockwood Morris and Malcolm Newey. Paulson's historical commentary records this sequence of collaborators, and Gordon's own account connects the earlier Stanford system to the Edinburgh work and then to HOL. Dana Scott's logic supplied the original object of mechanisation.

ML—originally “Meta Language”—made proof procedures programmable. Terms, formulae, goals and strategies could be handled as data and functions. Milner's polymorphic type discipline, later analysed with semantic and syntactic soundness results and Algorithm W, became a major programming-language contribution in its own right. But the historical credit should remain precise: LCF, ML, tactic design and interactive theorem proving grew through a team and a research community, even though Milner's architectural insight was central enough to form part of his 1991 ACM Turing Award citation.

Forward inference and backward search then acquired distinct roles. An inference rule consumes theorem values and returns a theorem value. A tactic looks at a goal and proposes subgoals. Its validation records how theorem values for those subgoals can be assembled into a theorem for the goal. Tacticals—higher-order combinators for sequencing, repetition and choice—organise tactics. They increase expressive power outside the protected construction boundary; they are not extra axioms.

That separation explains why a large search procedure need not be trusted in the same way as the theorem constructors. Search code can be replaced, tuned or abandoned while the acceptance interface remains comparatively stable. The useful analogy is not “automation is safe.” It is “automation may propose; only a smaller interface may confer the durable type.”

What the abstract type buys

An abstract data type hides its representation and exposes selected operations. Applied to theorems, the idea means that user code may hold a theorem value and pass it to sanctioned functions without fabricating another value by editing its internal fields. The language's type abstraction polices this boundary.

The assurance gain is architectural. Review can concentrate on a smaller collection of axioms and inference-rule implementations instead of every tactic ever written. New automation can be rich because its final products must still travel through that common route. The amount of code that is complicated is no longer identical to the amount of code that directly decides whether a theorem value exists.

“Small kernel” should not be romanticised into “no trust.” First, the axioms and rules must actually be sound for the intended logic. The abstract type prevents bypass; it does not certify that a primitive rule was chosen or programmed correctly. Second, type abstraction depends on the implementation preserving it. Compiler defects, unsafe escape hatches, runtime faults and hardware errors sit below the logical interface. Third, parsers and printers can mislead users even when the stored theorem value was constructed correctly. The trusted base is narrowed, not abolished.

Nor is kernel soundness the same as logical consistency. Sound primitive rules preserve validity relative to a semantics or formal account; a consistency claim concerns whether contradiction is derivable. The relationship depends on assumptions that an abstract type alone does not discharge. Saying “this value could only be built through these functions” is a provenance claim about construction. It is not an independent proof that every function embodies a valid rule.

The same caution separates proof from specification. A theorem about a model establishes a consequence within that formalisation. It does not establish that the model captures the intended system, environment, threat, regulation or human decision. If the specification omits a real constraint, a flawless kernel can prove the wrong formal question perfectly. Verification strengthens an explicit contract; it cannot supply the missing intent.

Why validation is the hinge

The validation function is easy to flatten into a generic “check,” but its role is more exact. A tactic performs a backward transformation: from one goal to a list of subgoals. The validation goes forward: given theorem values for those subgoals, it constructs the theorem for the original goal. Backward search therefore carries with it a deferred account of how success will be justified.

This makes a proof-state transition more than a visual change in an interface. A procedure that merely deletes a goal has not proved it. A procedure that returns an empty subgoal list must also supply a validation able to produce the goal's theorem without invented premises. If the promised assembly is invalid, the final forward construction fails.

Tacticals preserve this discipline while composing strategies. A sequential tactical can apply one tactic and then another to the resulting subgoals; a repetition tactical can continue while progress is possible. Their composition must also compose the validations. The control layer can become elaborate, but the acceptance evidence follows the structure back to the primitive inference operations.

This is the point of the opening scene. A search log, a green status and a polished script are useful records, but they are not the theorem value. In modern engineering language, activity evidence and acceptance authority have been deliberately separated. The boundary is not impressed by the amount of computation; it asks whether the protected constructors can reproduce the claimed conclusion from accepted premises.

Descendants are related, not identical

The LCF approach influenced a broad family of provers. Gordon carried the architectural lineage into HOL, while Paulson developed Cambridge LCF and then Isabelle. Cambridge's account of HOL Light still describes an extensible system whose soundness rests on a small trusted core. These are genuine descendants.

Inheritance does not mean uniformity. Paulson's account of Isabelle says its rules and proof states share a representation and that its forward and backward reasoning rest on principles different from classic LCF's function-per-rule design. Systems based on constructive type theory may retain proof terms and rely on a type checker in another way. Some systems export certificates for independent checking. Even within the LCF tradition, choices about unsafe features, proof recording, kernel language and rechecking alter the trusted base.

The careful claim is therefore historical and architectural: Milner and the Edinburgh team showed how strong type abstraction could separate extensible proof search from protected theorem construction. Many later systems adapted that lesson. It would be inaccurate to say that every modern proof assistant implements the same small kernel, or that the mere use of tactics identifies an LCF architecture.

Sources and limits

This article uses original publications, university archives and technical retrospectives. It does not audit a current prover or claim a measured kernel size. The final governance analogy—keep the common acceptance rule minimal and verifiable while leaving future search methods open—is an editorial reading informed by Lu Heng's minimum-initial-specification principle, not a claim about Milner's political or institutional views.