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.