Why do we believe the Church-Turing Thesis? The Church-Turing Thesis, which says that the Turing Machine model is at least as powerful as any computer that can be built in practice, seems to be pretty unquestioningly accepted in my exposure to computer science.  Why?  Do we have any more evidence for its truth than "nobody has been able to think of a more powerful model than Turing's yet?"  If so, why do we accept that argument as truth?  It seems to me that in any other mathematical discipline, a claim like the Church-Turing thesis whose support amounts to "we haven't yet found a counterexample" would not be taken seriously by the community.
 A: The Church-Turing thesis is credible because every singe model of computation that anyone has come up with so far has been proven to be equivalent to turing machines (well, or strictly weaker, but those aren't interesting here). Those models include


*

*Recursive functions over the integers

*The lambda calculus

*Combinatory logic


and many more. It's indeed hard to imagine anything algorithm-like which cannot be formalized in any of these models.
The difference between the Church-Turing thesis and real theorems is that it seems impossible to formalize the Church-Turing thesis. Any such formalization would need to formalize what an arbitrary computable function is, which requires a model of computation to begin with. You can think of the Church-Turing thesis as a kind of meta-theorem which states

Whenever you pick some intuitive notation of computable and formalize it, the resulting model of computation is either equivalent to turing machines, or strictly weaker.

All concrete instances of this meta-theorem that haven been encountered haven been proven. We do know that all the models of computation listed above are equivalent. Since we cannot prove the meta-theorem, for the reason stated above, we thus cannot do any better than say "Well, we don't see how it could not be true, so we'll assume it's true".
A: A side note: I think it is an error to identify the Church-Turing Thesis with a claim about what machines can do in practice. Some reflections [if I may be forgiven self-quotation.]
(a) It is important to note that there are three levels of concept that are in play here when we talk about computation.


*

*At the pre-theoretic level – and guided by some paradigms of common-or- garden real-world computation – there is a loose cluster of inchoate ideas about what we can compute with paper and pencil, about what a com- puter (in the modern sense) can compute, and about what a mechanism more generally might compute.

*Then at what we might call the proto-theoretic level we have, inter alia, one now familiar way of picking out strands from the pre-theoretic cluster while idealizing away from practical limitations of time or amount of paper, giving us the notion of an effectively computable function. So here some theoretic tidying has already taken place, though the concept still remains somewhat vaguely characterized (what makes a step in a step-by-small-step algorithmic procedure ‘small’ enough to be admissible?).

*Then at the fully theoretic level we have tightly characterized concepts like the concept of a recursive function and the concept of a Turing-computable total function.
It would be quite implausible to suppose that the inchoate pre-theoretic cluster of ideas at the first level pins down anything very definite. No, the Church–Turing Thesis sensibly understood, in keeping with the intentions of the early founding fathers, is a view about the relations between concepts at the second and third level. The Thesis kicks in after some proto-theoretic work has been done. The claim is that the functions that fall under the proto-theoretic idea of an effectively computable function are just those that fall under the concept of a recursive function and under the concept of a Turing-computable function. NB: the Thesis is a claim about the extension of the concept of an effectively computable function.
(b) There are other strands in the pre-theoretic hodgepodge of ideas about computation than those picked up in the idea of effective computability: in particular, there’s the idea of what a machine can compute and we can do some proto-theoretic tidying of that strand too. But the Church–Turing Thesis is not about this idea. It must not be muddled with the entirely different claim that a physical machine can only compute recursive functions – i.e. the claim that any possible computing mechanism (broadly construed) can compute no more than a Turing machine. For perhaps there could be a physical set-up which somehow or other is not restricted to delivering a result after a finite number of discrete, deterministic steps, and so is enabled to do more than any Turing machine. Or at least, if such a ‘hypercomputer’ is impossible, that certainly can’t be established merely by arguing for the Church–Turing Thesis.
Let’s pause over this important point, and explore it just a little further. It is familiar that the Entscheidungsproblem can’t be solved by a Turing machine. In other words, there is no Turing machine which can be fed (the code for) an arbitrary first-order wff, and which will then decide, in a finite number of steps, whether it is a valid wff or not. Here, however, is a simple specification for a non-Turing hypercomputer that could be used to decide validity.
Imagine a machine that takes as input the (Gödel number for the) wff $\varphi$  which is to be tested for validity. It then starts effectively enumerating (numbers for) the theorems of a suitable axiomatized formal theory of first-order logic. We’ll
suppose our computer flashes a light if and when it enumerates a theorem that matches $\varphi$ . Now, our imagined computer speeds up as it works. It performs one operation in the first second, a second operation in the next half second, a third in the next quarter second, a fourth in the next eighth of a second, and so on. Hence after two seconds it has done an infinite number of tasks, thereby enumerating and checking every theorem to see if it matches $\varphi$ ! So if the computer’s light flashes within two seconds, $\varphi$  is valid; if not, not. In sum, we can use our wildly accelerating machine to decide validity, because it can go through an infinite number of steps in a finite time.
Now, you might very reasonably think that such accelerating machines are a mere philosophers’ fantasy, physically impossible and not to be taken seriously. But actually it isn’t quite as simple as that. For example, we can describe space-time structures consistent with General Relativity which apparently have the following feature. We could send an ‘ordinary’ computer on a trajectory towards a spacetime singularity. According to its own time, it’s a non-accelerating com- puter, plodding evenly along, computing forever and never actually reaching the singularity. But according to us – such are the joys of relativity! – it takes a finite time before it vanishes into the singularity, accelerating as it goes. Suppose we set up our computer to flash us a signal if, as it enumerates the first-order logical theorems, it ever reaches $\varphi$. We’ll then get the signal within a bounded time just in case $\varphi$  is a theorem. So our computer falling towards the singularity can be used to decide validity.
Now, there are quite fascinating complications about whether this fanciful story actually works within General Relativity.  But no matter. The important point is that the issue of whether there could be this sort of Turing-beating physical set-up – where (from our point of view) an infinite number of steps are executed – has nothing to do with the Church–Turing Thesis properly under- stood. For that is a claim about effective computability, about what can be done in a finite number of steps following an algorithm.
A: We do have something other than examples to justify the Church-Turing thesis. Turing's original paper contains a detailed argument that any function which can be algorithmically computed by a human can be computed by a Turing machine. The question whether this argument is a "formal proof" misses the point that Turing's argument is exactly the type of argument that is needed to justify the claim. Indeed, a key motivation for continuing to define Turing machines in computability (rather than using only more convenient models of computation) is that Turing machines are the model that is most amenable to a justification of the Church-Turing thesis, because they are directly inspired by the method of an algorithmic human computer. 
A: The idea is that you can write an interpreter for any Programming Language using Turing Machines i.e. there is a Turing Machine that will interpret any program written in any given Programming Language and execute what it would.
It is believed because all programming Languages must be executable by a computer and all a computer does is compare characters and set values based on what equals what and that is what Turing Machines do!
