 However, Turing certainly did not prove that no such machine can be specified. All that Turing’s results tell us is that if there is such a machine, then it is not a Turing machine. It is also worth mentioning that, although the Halting Problem is very commonly attributed to Turing (as Langton does here), Turing did not in fact formulate it. The Halting Problem originated with Martin Davis, probably in 1952 (Davis 1958: 70).