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
  • (23 questions)
• 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
  • (Influenced by ALGOL)
• 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 SM_FORCES)
• 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
  • Used HACL*, which is written in F*
  • https://jonathan.protzenko.fr/2025/04/18/python.html

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
• 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