An attempt to know what happened when and what influenced development of what, in the field of logic and verified software.
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
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
1956: Kleene's theorem
- Representation of events in nerve nets and finite automata - Kleene (1956 or is it 1951??)
- (Language accepted by finite automata and regex are same)
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) ˡ
1960: Davis-Putnam algorithm
- (Check SAT of a first oder formula via resolution)
1961: Glushkov automata construction
- The abstract theory of automata - V. Glushkov (1961)
1962: DPLL algorithm
- (Davis-Putnam-Logemann-Loveland algorithm)
1962: Scott encoding
1964: Brzozowski derivatives
- Derivatives of regular expressions - Janus Brzozowski (1964)
1967: Automath
- (By N. G. de Bruijn and others)
1971: Cook-Levin theorem
- (Boolean SAT is NP-complete)
1971: Martin-Löf type theory
- (Intuitionistic type theory by Per Martin-Löf)
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)
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)
1985-1987: Therac-25 causes patient deaths by excess radiation ˡ
- (A computer-controlled radiation therapy machine)
1988: The calculus of constructions - Coquand, Huet, Gérard
1991: Barengredt's lambda cube
- Introduction to generalized type systems - Hendrik P. Barendregt (1991)
1993: Mars climate orbiter bug
- (English units vs metric unit confusion in SMFORCES)
1996: Ariane 5 failure
1999-2015: British Post Office scandal
- Errors in Horizon software by Fujistsu led to false accustations 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<)
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)
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)