 Gödel eventually held up Turing’s analysis as a better model of computation precisely because Turing justifies the identification of intuitive computation with Turing machine computation on the basis of a detailed analysis of what a human computer, equipped with paper and pencil, must actually do (Turing 1936: §9). It seems that a counterpart of Turing’s compelling analysis has yet to be given for the case of λ-computation. It should be emphasized, however, that Church’s main aim was not to defend an analysis of computability but rather to set the stage for a proof that a particular number theoretic combinatorial problem is not solvable. So long as computation is defined as a finite process, cardinality considerations imply that non-computable functions must exist, and Church wished to demonstrate that his combinatorial problem was one of these.