Before computers existed, Alonzo Church invented a language made of nothing but functions, and used it to prove that some problems can never be solved by any machine. He began developing lambda calculus in the late 1920s and published the first version in 1932–33 as part of an attempt to rebuild the foundations of logic without Russell’s theory of types. With his students he showed that lambda-definable functions capture exactly the same class of functions as Gödel’s general recursive functions. In 1936 he used this to prove there is no algorithm that can decide every problem in elementary number theory (and later that first-order logic is undecidable). That same year Alan Turing arrived at Princeton; they quickly proved lambda calculus and Turing machines have the same computational power. This equivalence is the Church–Turing thesis. Lambda calculus treats everything as a function: numbers (Church numerals), Boolean logic, lists, and even recursion (via the Y combinator). Because functions are first-class and can be applied to other functions, it became the mathematical basis of functional programming. Lisp borrowed the λ notation; later languages such as Scheme, ML, OCaml, and Haskell are far closer to the original calculus. In 1940 Church published “A Formulation of the Simple Theory of Types,” combining lambda calculus with a simple type hierarchy. That paper is the direct ancestor of modern type theory and of the type systems used in functional languages and proof. Together with Turing machines, lambda calculus is one of the two original models of computation. One is mechanical and tape-based; the other is purely functional. Both still shape how we think about programs.