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
- (Euclidean geometry)
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)
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
- (23 questions)
1901: Russell's paradox
- (Had already been discoverd 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')
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)
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: Turing machine (Turing)
- (On Computable Numbers With an Application 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
1945: von-Neumann architecture
- First published description of stored program architecture
- First draft of a report on the EDVAC

1958: ALGOL
- (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)

1962: DPLL algorithm
- (Davis-Putnam-Logemann-Loveland algorithm)
1962: Scott encoding

1964: SECD machine by Landin ᵈ
- Mechanical evaluation of expressions - Peter J. Landin (1964)
- 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.
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
1969: Logic of Computable Functions (LCF) by Dana Scott
- (This work was published only in 1993)
1970: Pascal
- (Influenced by ALGOL)
1971: Denotational semantics
- Toward a mathematical semantics for computer languages - Dana Scott, Christopher Strachey
- aka Scott-Strachey semantics
1971: Cook-Levin theorem
- (Boolean SAT is NP-complete)
1971: Martin-Löf type theory
- (Intuitionistic type theory by Per Martin-Löf)
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
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)
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: 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
1987: Edinburg LF
- (aka LF)
- (Harper, Honesell, Plotkin)
1988: The calculus of constructions - Coquand, Huet, Gérard
1989: First version of modern Coq
- (Version 4.10)
- (With support for tactics??)
- (To be renamed Rocq in 2025)
1990: Haskell programming language
1991: Barengredt's lambda cube
- Introduction to generalized type systems - Hendrik P. Barendregt (1991)
1991: Python programming language
1993: Mars climate orbiter bug
- (English units vs metric unit confusion in SM_FORCES)
1993: OCaml
1995: Racket
- (Initiated by a group led by Matthias Felleisen)
1996: Ariane 5 failure
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
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<)
2007: Agda2
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)
2015: Rust programming language
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??)

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)
- http://jmc.stanford.edu/articles/lisp/lisp.pdf

DBT

Original UTLC had a problem related to Russell's paradox. How? (src: pat wadler)
- Self application
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 ??