 As a principle, Church’s Thesis has a somewhat curious status. It appears to be a basic principle. On the one hand, the principle is almost universally held to be true. On the other hand, it is hard to see how it can be mathematically proved. The reason is that its antecedent contains an informal notion (algorithmic computability) whereas its consequent contains a purely mathematical notion (Turing machine computability). Mathematical proofs can only connect purely mathematical notions—or so it seems. The received view was that our evidence for Church’s Thesis is quasi-empirical. Attempts to find convincing counterexamples to Church’s Thesis have come to naught. Independently, various proposals have been made to mathematically capture the algorithmically computable functions on the natural numbers. Instead of Turing machine computability, the notions of general recursiveness, Herbrand-Gödel computability, lambda-definability… have been proposed. But these mathematical notions all turn out to be equivalent. Thus, to use Gödelian terminology, we have accumulated extrinsic evidence for the truth of Church’s Thesis.