3 ms·

Right, IIUC type theory started as Bertrand Russell's attempt to do exactly that (and follow through the ramifications - you can't "just" anything in math). Th

• nl 7y ago
  Then suddenly, Haskell. Sequence of events: Russell publishes Principia Mathematica (1910-1913) David Hilbert studies Principia Mathematica, and keeps working on open questions from it (1913 onwards): He poses the proof of the consistency of arithmetic (and of set theory) again as the main open problems. In both these cases, there seems to be nothing more fundamental available to which the consistency could be reduced other than logic itself. And Hilbert then thought that the problem had essentially been solved by Russell’s work in Principia. Nevertheless, other fundamental problems of axiomatics remained unsolved, including the problem of the “decidability of every mathematical question,” which also traces back to Hilbert’s 1900 address. These unresolved problems of axiomatics led Hilbert to devote significant effort to work on logic in the following years. In 1917, Paul Bernays joined him as his assistant in Göttingen. In a series of courses from 1917–1921, Hilbert, with the assistance of Bernays and Behmann, made significant new contributions to formal logic.[1] In 1928 Haskell Curry moved to Germany to study under David Hilbert Curry's work developed into the Curry–Howard correspondence[2] which led to the language being named after him. [1] https://plato.stanford.edu/entries/hilbert-program/#1.2 https://plato.stanford.edu/entries/hilbert-program/#1.2 [2] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Origin,_scope,_and_consequences https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...