 Church was the first to devise a formalism—the λ-calculus—within which it was possible to define a class of functions that coincide, arguably, with the intuitively computable functions—those that can be evaluated by means of an algorithm, i.e., a computer program. He also provided, again arguably, the first example of a particular significant function that is not computable. (Other examples, due independently to Kleene (1936) and Turing (1936) followed quickly.) He did this by constructing a function that is provably not recursive in the sense defined slightly earlier by Gödel and Herbrand. He then appealed to the assumption that any intuitively computable function is recursive to conclude that the function in question is not computable—in Church’s terminology it is not effectively calculable. (We will continue to use the terms “computable” and “intuitively computable” rather than “effectively calculable” since they are more readily understood by non-specialists.) Given the nature of this function, this meant that a certain problem of elementary number theory is unsolvable: there is no way it could be solved by algorithmic means. It also implied a negative solution to the Entscheidungsproblem first enunciated by Hilbert and Ackerman (1928): the problem whether there is a decision procedure for first order logic. The italicized assumption later came to be known as “Church’s thesis” (Kleene 1952).