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.
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.