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