An attempt to know what happened when and what influenced development of what, in the field of logic, programming language theory and verified software.
Timeline
- 350BC: Syllogisms
- (In Aristotle's Prior analytics)
- 300BC: Euclid's Elements
- 1347: Ockham's razor
- (Old concept got some more attention at this point)
- (Prefer the proof with the smallest number of assumptions)
- ('Simplest explanation is usually the best one')
- (Russell: 'Whenever possible, substitute constructions out of known entities for inferences to unknown entities')
Modern
- 1847: Boolean algebra developed
- Mathematical Analysis of Logic - George Boole (1847)
- The Laws of Thought - George Boole (1854)
- 1872: 'Ignoramus et ignorabimus' quote by du Bois-Reymond
- 'We don't know and we shall not know'
- About the sum of all human knowledge
- 1879: Begriffschrift by Gottlob Frege published
- (Hilbert system: Reliant on axioms)
- (First-order symbolic logic)
- 1891: Cantor's diagonal argument
- (Proves that there are uncountable sets)
- (ℝ is uncountable)
- 1900: Hilbert's problems posed
- 1901: Russell's paradox
- (Had already been discovered by Ernst Zermelo in 1899)
- 1905: Richard's paradox
- 1908: Russell's type theory
- (Proposed to avoid Russell's paradox)
- 1908: Zermelo set theory
- (Proposed to avoid Russell's paradox)
- (First axiomatic set theory)
- (Till this point it was all informally defined naïve set theory)
- 1910: Principia Mathematica - Whitehead and Russell
- (Showed that 'formal logic could express a large part of mathematics'¹)
- 1920: Schönfinkel's work on combinatory logic
- 1921: Hilbert defines Hilbert's program
- 1928: Entscheidungsproblem posed (Hilbert, Ackermann)
- (Given all axioms of math, is there an algorithm to check if a proposition is universally valid?)
- (Required a formal definition of an algorithm or computability)
- ('Entscheidungsproblem' is German for 'decision problem')
- Grundzuge der theoretischen logik - Hilbert, Ackermann (1928)
- 1929: Gödel's completeness theorem
- (First order logic is complete. There is a first order formula for all first order truth)
- (Proof simplified by Henkin in 1949)
- (Henkin's proof was in turn simplified by Hasenjaeger in 1953)
- 1930: Curry's work on Combinatory logic
- (Based on earlier work of Schönfinkel)
- 1930: "Wir müssen wissen. Wir werden wissen" quote by Hilbert
- We must know. We shall know
- A later iteration of the same conference were du Bois-Reynold gave his comment
- 1931: Gödel's incompleteness theorems
- (2 theorems)
- (Showed limitations of formal systems)
- (Showed that Hilbert's program was impossible)
- Über formal unterscheidbare Sätze der Principia Mathematica und verwandter Systeme I - Gödel (1931)
- 1932: Original lambda calculus (Church)
- (Originally meant to encode logical formulas, but that didn't work out due to inconsistency as shown by Church-Rosser paradox)
∃x, A[x] could be written as Σ(λx. A[x]) (What did Σ mean ???)- A set of postulates for the foundation of logic - Alonzo Church (2 parts: 1932, 1933)
- (The 1932 paper had this prophetic remark: 'There may, indeed, be other applications of the system than as its use as a logic')
- 1934: Natural deduction and sequent calculus (Gentzen)
- Untersuchungen über das logische Schließen - Gerhard Gentzen (1935)
- aka Investigations in Logical Deduction
- (Introduced ∀ for universal quantification to match ∃ of Peano)
- (Unlike Hilbert system, natural deduction relies inference rules. Axioms are 0-ary inference rules)
- (System LJ: Intuitionistic logic as sequent calculus)
- (System LK: Classical logic as sequent calculus)
- (Cut-elimination theorem in sequent calculus: There is a 'cut-free' proof for all 'cut' proofs )
- (Both natural deduction and sequent calculus are equivalent)
- 1935: Kleene-Rosser paradox
- (Original LC is inconsistent)
- The inconsistency of certain formal logics - Kleene, Rosser (1936)
- (Church originally meant lambda calculus as a way to encode logic, but this paradox played spoilsport)
- (Yet, by this time it was obvious that lambda calculus was of independent interest)
- (Curry's combinatory logic and original lambda calculus are inconsistent)
- (Curry himself later simplified this as Curry's paradox)
- 1936: Church encoding ??
- An unsolvable problem in number theory - Alonzo Church (1936)
- 1936: Church's result on the Entscheidungsproblem
- A note on the Entscheidungsproblem - Alonzo Church (1936)
- 1936: Turing machine (Turing)
- (On Computable Numbers With an Application to the Entscheidungsproblem)
- An answer to the Entscheidungsproblem
- 1936: General recursive functions (Gödel, Kleene)
- (Gödel's lectures at Princeton were made in 1934, Kleene made notes and published it in 1936)
- General recursive functions of natural numbers - Stephen Cole Kleene (1936)
- 1936: Church-Turing thesis
- (Turing machine and lambda calculus are equivalent)
- (Entscheidungsproblem proven impossible)
- (Turing and Church found this independently)
- (1937: Computability and λ-definability - Alan Turing)
- 1936: Church-Rosser theorem
- (Lambda calculus is confluent)
- (Normal form of lambda calculus terms)
- 1940: Simply typed lambda calculus
- (Weaker than UTLC, but logically consistent)
- A formulation of the simple theory of types - Alonzo Church (1940)
- 1942: Curry's paradox
- 1942: Plankalkül by Konrad Zuse
- The first high-level language for computers
- 1945: von-Neumann architecture
- First published description of stored program architecture
- First draft of a report on the EDVAC
- 1954: FORTRAN
- Led by John Backus
- "what FORTRAN did primarily was to mechanize the organization of loops" - John Backus
- 1955: Second order logic can encode HOL
- Reductions in the Theory of Types - Hintikka, K. Jaakko J. (1955)
- 1958: ALGOL
- Invovled Peter Naur, John Backus, John McCarthy
- (Algol 60 report introduced Backus-Naur Form)
- (Algol 68: Quite different. Considered too complex to implement)
- (Algol 60 was the most popular ALGOL)
- (Algol 60 introduced the modern if-then-else syntax) ˡ
- 1960s: Continuations
- Earliest description in literature was by Adriaan van Wijngaarden
- A survey: The discoveries of continuations - John. C. Reynolds (1993) ˡ
- 1960: Davis-Putnam algorithm
- (Check SAT of a first oder formula via resolution)
- 1960: Design of Lisp published
- Recursive functions of symbolic expressions and their computation by machine, Part I - John McCarthy
- (Steve Russell would soon write a form of lisp interpreter on an IBM 704)
- (
car and cdr are assembly macros for IBM 704)
- Lisp was an implementation of lambda calculus
- McCarthy developed the idea of conditional statement (
if) while working on lisp
- 1962: Abstract syntax
- Term coined by John McCarthy
- Towards a mathematical science of computation - John McCarthy
- 1962: DPLL algorithm
- (Davis-Putnam-Logemann-Loveland algorithm)
- 1962: Scott encoding
- 1964: SECD machine by Landin ᵈ
- Mechanical evaluation of expressions - Peter J. Landin (1964)
- (This paper also introduced indentation sensitivity in programs ???)
- Stands for internal registers of the machine: Stack, Environment, Control, Dump
- First abstract machine for lambda calculus
- Landin also coined the name 'closure' of functions in this paper.
- 1965: A correspondence between ALGOL 60 and Church's lambda-notation: Part I - Landin
- Possibly the first instance where denotational semantics was given to a programming language
- SECD can be thought of as an operational semantics
- 1966: APL
- Based on a mathematical notation for modeling arrays ʷ
- 1966: The next 700 programming languages - Landin
- It was foreseen that lot many more languages would be made
- ISWIM: If you see what I mean (a language design)
- Church without lambda
- Never implemented
- Had patmat, garbage collection, etc
- Primitives or domain specific languages
- 1966: Böhm-Jacopini theorem
- Flow diagrams, Turing machines and languages with only two formation rules - Corrado Böhm, Giuseppe Jacopini (1966)
- Structured programming
- 1967: Assigning meanings to programs - Robert W. Floyd [ˡ
- Logical assertions to verify programs
- Considered a pioneer paper on programming language semantics
- 1968: Operational semantics
- Used for defining semantics of ALGOL 68
- The name was coined later
- 1968: Automath
- The mathematical language AUTOMATH, its usage, and some of its extension - N. G. de Bruijn (1968)
- (First logical framework)
- 1968: Dijkstra's article crticising use of
goto statement
- Goto statement considered harmful - Edsgar W. Dijkstra (1968)
- 1969: Hoare logic
- An axiomatic basis for computer programming - Charles Antony Richard Hoare (1969)
- Axiomatic semantics
- Built on work by Floyd. Hoare logic is aka Floyd-Hoare logic
- 1969: Logic of Computable Functions (LCF) by Dana Scott
- (This work was published only in 1993)
- 1969: Curry-Howard isomorphism becomes clear
- The formulae-as-types notion of construction - William Howard (1969)
- Combinatory Logic, Volume I - Haskell Curry, Robert Feys (1958)
- Functionality in Combinatory Logic - Haskell Curry (1934)
- 1970: Pascal
- 1971: Denotational semantics
- Toward a mathematical semantics for computer languages - Dana Scott, Christopher Strachey
- aka Scott-Strachey semantics
- 1971: Martin-Löf type theory
- (Intuitionistic type theory by Per Martin-Löf)
- 1971: Work begins for Boyer-Moore theorem prover
- aka Nqthm
- By Robert Boyer and J Moore
- Was a predecessor of ACL2
- 1972: Structured programming
- Book by Dijkstra, Hoare and Dahl
- 1972: C programming language
- 1972: Prolog programming language
- 1972: Stanford LCF
- (Robin Milner's implementation for LCF)
- (No support for custom proof commands)
- (Hogged up memory)
- 1972: Girard's paradox
- (Type theory version of Russell's paradox)
- (Martin-Löf's original type theory is shown to be inconsistent due to Type in Type)
- 1973: Mizar theorem prover
- Guarded commands, nondeterminacy and formal derivation of programs - Dijkstra (1975)
- A form of Hoare logic
- Introduced 'predicate transformer semantics'
- Uses weakest precondition
- 1976: Four colour theorem proven
- (First computer-assisted major proof)
- (By Kenneth Appel, Wolfgang Haken of University of Illinois)
- (A discussion is at [3])
- (Several mistakes were found later?? but were all addressed)
- Every planar map is four-colorable - Appel, Haken (1989)
- 1977: Safety and liveness properties
- Proving the correctness of multiprocess programs - Leslie Lamport (1977)
- 1977: Tail call optimization
- Debunking the "expensive procedure call" myth or, procedure call implementations considered harmful or, Lamdba: The ultimate goto - G. L. Steele
- (Part of 'The Lambda papers')
- 1977: Algebraic data types
- Design considerations for a functional programming language - R. Burstall (1977, as part of NPL)
- HOPE: An experimental applicative language - R. M. Burstall, D. B. MacQueen, D. T. Sannella (1980)
- 1978: ML
- (A general purpose, higher order programming language)
- (Made for use in Edinburgh LCF)
- A theory of type polymorphism in programming - Robin Milner
- (Had a 'novel polymorphic type system')
- 1979: Edinburg LCF
- (By Milner and his associates at University of Edinburg)
- (An LCF implementation embedded in ML)
- ('proof is always performed', but exists 'only ephemerally as part of evaluation process' => less memory usage than Stanford LCF)
- 1980s: Krivine machine (aka K-machine) ᵈ
- Call-by-name abstract machine for lambda calculus
- Was formally published only years after its invention
- A call-by-name lambda-calculus machine - J. L. Krivine (2007)
- By Jean-Louis Krivine
- Operational semantics ??
- 1984: Literate programming
- Literate programming - Donald Knuth (1984) (Used a language called WEB)
- 1984: Work started on an implementation of CoC
- (This would later become Coq)
- (Gérard Huet and Thierry Coquand are invovled)
- 1985-1987: Therac-25 causes patient deaths by excess radiation ˡ
- (A computer-controlled radiation therapy machine)
- 1985: C++ programming language
- 1986: Isabelle prover released
- 1987: Edinburg LF
- (aka LF)
- (Harper, Honesell, Plotkin)
- 1988: The calculus of constructions - Coquand, Huet, Gérard
- 1988: Fuzzing
- Started with a class project in University of Wisconsin under Barton Miller
- An automated software testing technique
- 1989: Type classes in Haskell
- How to make ad-hoc polymorphism less ad-hoc - Philip Wadler and Stephen Blott
- 1989: First version of modern Coq
- (Version 4.10)
- (With support for tactics??)
- (Renamed Rocq in 2025)
- 1990: ACL2 theorem prover
- A Computational Logic for Applicative Common Lisp
- By Robert Boyer, J Moore, Matt Kaufmann
- 1990: Haskell programming language
- 1991: Barengredt's lambda cube
- Introduction to generalized type systems - Hendrik P. Barendregt (1991)
- 1991: Python programming language
- 1993: Use of monads to model effects in programming languages
- Imperative functional programming - Simon Peyton Jones and Philip Wadler (POPL 1993)
- 1993: Mars climate orbiter bug
- (English units vs metric unit confusion in SMFORCES)
- 1993: OCaml
- 1994: Intel Pentium FDIV bug discovered
- By Prof. Thomas Nicely at Virginia
- 1995: Racket
- (Initiated by a group led by Matthias Felleisen)
- 1996: Ariane 5 test flight failure
- Cause type conversion from 64-bit float to 16-bit int
- 1998: ACL2 used to prove correctness of AMD K5 FPU
- A mechanically checked proof of the AMD5K86TM floating-point division program - J Strother Moore, Thomas W. Lynch, Matt Kaufmann (1998)
- Work done in the wake of the recent Pentium FDIV bug
- 1998: SSA is functional programming - Andrew Appel (1998)
- 1999: Twelf
- Twelf - A meta-logical framework for deductive systems - Frank Pfenning, Carsten Schürmann
- (An implementation of LF)
- 1999-2015: British Post Office scandal
- Errors in Horizon software by Fujistsu led to false accusations of theft
- 2002: Separation logic
- Local reasoning about programs that alter data structures - Peter O'Hearn, John Reynolds, Hongseok Yang (2001)
- Separation logic: A logic for shared mutable data structures - John Reynolds (2002)
- 2003: Generalized Algebraic Data Type (GADT)
- First-class phantom types - James Cheney, Ralf Hinze (2003)
- Guarded recursive datatype constructors - Hongwei Xi, Chiyan Chen, Gang Chen (2003)
- Silly type families - Lennart Augustsson, Kent Petersson (1994)
- 2005: Felt-Thompson proof of Four colour theorem made in Coq (Gonthier, et al)
- 2005: CompCert
- (C compiler formally verified with Coq. Considered first such effort for a 'realistic' compiler)
- 2005: POPLMark challenge
- (Ways to mechanise System F<)
- 2006: Gradual typing
- Combine aspects of static and dynamic typing
- Gradual typing for functional languages - Jeremy Siek, Walid Taha (2006)
- 2007: Agda2
- 2007: Concurrent separation logic (CSL)
- 2009: seL4: microkernel made with Isabelle/HOL
- 2012: Odd order theorem proven in Coq (Gonthier, et al)
- 2014: CakeML
- (Compiler for a subset of sml, formally verified with HOL4)
- 2014: Shellshock vulnerability of bash
- Found via a fuzzing tool named AFL
- 2014: Heartbleed vulnerability in OpenSSL
- Cause: Missing bound check allowing erroneous memory access
- 2015: Rust programming language
- 2015: iris
- (A framework for concurrent seperation logic)
- 2018: Problems in Boeing 737 MAX surface
- (An automatic system named MCAS had problems??)
- (Faulty sensor data triggered MCAS at inappropriate time)
- 2023: PureCake
- (Compiler for PureLang, a haskell-like language, formally verified with HOL4.)
- (An effort to have something like cakeml but with laziness??)
- 2025: Formal verification of components in hashlib of Python stdlib
Refs
[1]: Propositions as types - Philip Wadler[2]: The Automation of Proof: A Historical and Sociological Exploration - Donald Mackenzie[3]: The Use of the Computer in the Proof of the Four Color Theorem - Kenneth I. Appel[4]: History of interactive theorem proving - John Harrison, Josef Urban and Freek Wiedijk[5]: History of Lisp - John McCarthy (1979)
- The history of Standard ML - David Macqueen, Robert Harper, John Reppy (HOPL, 2020)
- A history of Haskell: Being lazy with class - Simon Peyton Jones, Paul Hudak, John Hughes, Philip Wadler
DBT
- Original UTLC had a problem related to Russell's paradox. How? (src: pat wadler)
- Example of a typed lambda calulus with provision for general recursion
- Can such a system be useful for proofs? Can't anything be proven?
- Schmidt found an error in original computer generated proof of four colour theorem ??