That's certainly a very language-and-logic perspective on things. But one of the reasons Church missed the general concept of computation whereas Turing didn't was precisely because Church was stuck in the formalism of logic, and couldn't recognize that computation extends well beyond it. So proofs are programs, but so are, say, metabolic networks, neuron networks, and just about any discrete dynamical system. But are metabolic networks proofs? That's not so clear, and therefore it's not so clear that there is a universal equivalence here.
Its the program itself that is the proof, not the computer running the program.
In a sufficiently powerful type system you can express any proposition as a function type. A proof of that proposition is also a program. The proof checker is a type checker. If your proof is invalid, your program won't type-check.
But what if the program that runs the proof will never terminate? For example I could write a 'proof' for some property of natural numbers by just iterating through all of them and every time validating the property.
Isn't a proof only valid if it can be validated within a reasonable amount of time, either by some human or by a computer?
Quoting from Wikipedia:
"Because of the possibility of writing non-terminating programs, Turing-complete models of computation (such as languages with arbitrary recursive functions) must be interpreted with care, as naive application of the correspondence leads to an inconsistent logic. The best way of dealing with arbitrary computation from a logical point of view is still an actively debated research question, but one popular approach is based on using monads to segregate provably terminating from potentially non-terminating code (an approach that also generalizes to much richer models of computation,[6] and is itself related to modal logic by a natural extension of the Curry–Howard isomorphism[ext 1]). A more radical approach, advocated by total functional programming, is to eliminate unrestricted recursion (and forgo Turing completeness, although still retaining high computational complexity), using more controlled corecursion wherever non-terminating behavior is actually desired."
That is not what programs as proofs means. It is not that the program finds or performs the proof; the program is the proof, in a certain formal sense. The thing it proves is its type. The validation step is type-checking. For most programming languages, type-checking is decidable, so testing whether the proof is valid is fine. However, most programming languages correspond to trivial proof systems (every type is inhabitable, so every proposition is provable).
This is part of the problem with proofs-as-programs: it's a beautiful theory, and inspires a lot of useful work, but if taken too literally it's wrong and useless.
What about programs that, by design, run indefinitely and do useful things? Say, a server that just responds to requests as they come. Is that "not a real program" for purposes of CH?
Or what about ones with side effects?
It seems to assume away a lot of (what is called) programs in actual practice.
There are accounts of infinitely-running programs as proofs; they have to do with the proof technique of conduction, which has to do with proving properties of infinite data structures; a counterpart of the more familiar technique of induction, which lets you prove things about finite data structures.
Side effects are a little harder to see proof-theoretically; for some effects there are reasonable stories (exceptions, for example, are a special case of continuations, which have connections to classical logic), but for many I think the story is still murky.
The Curry-Howard correspondence is more of a lens through which to approach PL theory, or an evolving research agenda, than it is a settled account of all programming practice.
As long as there is any structure or internal logic to what the program does, it can be reflected in its types.
For your example of a server, look at the Servant library in haskell. It allows you to define type safe routes and links, ensuring that your program exactly matches the API, and that no links are ever broken.
What is commonly known as Curry-Howard correspondence (the duality between programs/proofs, computing/math) actually goes way deeper.
The reason is that "computation" is very useful concept but it has taken us ages to define what it means precisely. But that didn't stop people of reinventing it in other areas.
Curry-Howard is only one of many other isomorphism between programs and other areas. See "Physics, Topology, Logic and Computation: A Rosetta Stone"[1] and in particular Table 4 on pg. 66. Curry-Howard correspondence is the last two columns of the table; the other three columns are other "correspondences" in topology, physics and category theory.
I'm not sure if you can really cast this as a debate between Church and Turing. It is certainly a difference between Brouwerian constructivism and this presentation of the Curry-Howard isomorphism. I think you'd be much happier with the (Brouwerian) realizability interpretation of logic. The idea here is that a proof is a (untyped) program, and types are predicates on programs. By Curry-Howard, propositions are certain special types, so this gives you a way of defining when a program p is a proof of a proposition A, written below as "p |= A". Here are some examples:
p |= A /\ B: if p evaluates to a pair of a proof of A and a proof of B.
p |= A -> B: if p implements a total function mapping proofs of A into proofs of B.
p |= exists n, A: if p evaluates to a pair of a number k and a proof of the statement A where n is replaced by k.
This is, for instance, implemented in NuPRL. It validates all laws of intuitionistic logic, but is also open ended. You can always add new axioms, so long as you can implement a realizer for them. E.g. if P is a boolean predicate on natural numbers, the statement "(~forall n, ~P n) -> exists n, P n" is true, since we can realize it using linear search, which terminates because of the assumption on P. Similarly, we have a realizer for the statement that "all function on real numbers are continuous", so what you get here is truly distinct from classical logic.
Of course, realizability has the problem that it already presupposes that you know how to show properties of arbitrary programs! On the other hand, if you have a proof for a positive statement you can always check the truth of special instances by running a program and looking at the results.
Anyway, to get back to your question. Under this interpretation, you can implement a proof on a metabolic network, in the same way as you can implement it using sticks and stones. Whether or not that has anything to do with the "Curry-Howard" correspondence is another question, though.
Are constructive realizers the same thing as C-H proofs, though? A realizer is indeed any Turing-computation that decides a proposition, but I don't think it's the same thing as a proof in the C-H sense. The latter must be a lambda expression or a term of some other typed formalism, rather than an arbitrary description of a Turing computation. I.e., you could implement a realizer for a proposition with a metabolic network, but the network is not a proof that it's the realizer you're looking for. In other words, I don't think you can reconstruct the proof from the realizer, once the realizer is no longer in the formalism of the proof and is just a TM. In fact, I think that the halting theorem precludes you from telling what proposition a TM realizes (if any), and so a TM can no longer be the proof of the original proposition it realizes. The two coincide, I think, only if the realizer is still expressed as a typed term.
And I didn't try to cast it as a debate between Church and Turing (which never existed, AFAIK), but to point out that equating programs with proofs is one rather narrow perspective of looking at programs. Arbitrary programs expressed in arbitrary ways are rarely proofs of anything (or anything nontrivial, that is), even if they happen to correspond realizers. I mentioned Turing to point out how this narrow view may result in missing out on fundamental qualities of computation.
I think historically the Curry-Howard correspondence grew out of the observation that combinatory logic and Hilbert proofs look very similar. There does not seem to be a large overarching story that doesn't makeup some history after the fact.
What I can say is that these days the Curry-Howard correspondence is typically taken to state that "Propositions are Types". And for typed languages, the difference between intrinsic types (Church style) and types as properties of programs (Curry style) are just two extremes on a very fluid spectrum.
You are absolutely right that this realizability interpretation as stated doesn't really help you define a complete notion of truth, since it doesn't solve the (unsolvable) problem of telling which proposition a program realizes. This is one of the reasons why Brouwer was so opposed to basing everything in mathematics on a system of inference rules. Without "intuition" about whether a particular program realizes a proposition you cannot really get off the ground.
My point isn't so much about a "notion of truth" (classical or intuitionistic), nor is it about "proofs as programs", but about "programs as proofs", which is really only true when programs are viewed narrowly, and in a specific formalism that Wadler is trying to promote. In other words, I take issue with presenting computation as equivalent to logic. The two obviously have things in common, and ideas flow in both directions, but presenting them as being one and the same, or two sides of the same coin, is misleading.
Are they not equivalent to computers running some program? Equivalence is transitive.
But I don't think you will be able to get any useful proof from one of them. That's because they are hard to program, they are still running some proof.
But a "computer running a program" is not an interesting proof of anything. The proof depends on how the program is written. For example, a program written in an untyped language encodes only a very trivial proof by the C-H correspondence (of `tt ⇒ tt` or something like that) even though it performs the same computation of a program written in another formalism that expresses a much more interesting proof. In other words, the proof does not lie in the dynamical process of computation, but in properties of the language used to express the computation. This is a much less universal claim.
I think that the common belief is that they are (or, at least, that a discrete model can capture their behavior), although I don't think it matters, as the common belief is that analog computers and digital computers have the same computational power.
What does it mean to say that analog and digital computers have the same computational power? My intuition would be something like: for any function calculable by an analog computer, for any desired degree of precision, there is a Turing-computable function which approximates it to that degree of precision. But you have to be a bit finnicky, since you can't actually feed an analogue input to a digital computer, either. So it has to be some relation between the precision of the input and the precision of the output. And of course there's the other direction, that analogue computers can simulate digital ones.
Do you know whether anything like this been formalized and proven?
Turing himself addressed this issue, and actually his famous 1936 paper talks about computing real numbers, not natural numbers. See http://cs.stackexchange.com/questions/35343/analog-computers... for a brief discussion. In short, we don't know of anything that an analog computer can do that a digital computer can't. If you think a bit about your point on precision, you'll see that "desired digital precision" actually covers a problem that is essential to the analog computation itself. In other words, try to think what "infinite precision" actually means.
But let me give an example that would make it more concrete. Suppose you want to build a computer that simulates the behavior of n bodies in gravitational interaction in space. It's obvious that with a digital computer, there would eventually be discrepancies between the actual system and the simulation (which would only grow). But now consider this: suppose that instead you want to do the simulation by building a "computer" which is nothing more than a copy of the original system (i.e., the "simulation" is composed of another set of n bodies in space). Is it possible to have this analog "simulation" more accurate than a digital simulation? The answer is no, because even supposing a true continuum of positions and velocities exists in the first place, in order to reconstruct the system precisely, you would need to pass an infinite amount of information to the "simulation", which is impossible.
