The calculus of constructions
In May 1986 Thierry Coquand and Gérard Huet of INRIA issued a report on the calculus of constructions, a higher-order formalism in which every proof is a lambda expression typed with the proposition it proves. Remove the types and what remains is the program corresponding to the proof. The authors proved strong normalisation: every computation terminates, so the logic is consistent.
Why it matters
A proof and a program became one object, and checking a proof became checking a type. Lean's kernel, its authors write, provides a version of the calculus of inductive constructions that rests on this work; in Lean, in 2024-2026, machines write and check proofs of olympiad problems and Erdős problems.
The report rests on the Curry-Howard correspondence between propositions and types and says that for computer science it yields a very high-level functional language in which a type can be an arbitrarily complex specification of a program. The terms, the authors say, are inspired by the Automath formalisms, with de Bruijn's indexes. The report has no measurement: it is a theory, not a system. The link to Lean rests on its authors' 2015 paper: Lean's kernel can provide a version of the calculus of inductive constructions, citing Coquand and Huet. What the record does not claim: when the first version of Coq was released; the documents read do not say.