I think it is applicable to "programs as proofs" (i.e. the opposite direction, which Wadler also makes), but more as an analogy. Once you say programs are proofs, then you reduce programs to logic, while computation is a natural (as well as mathematical) phenomenon that exists outside of any formalism.
I'm not sure that's true. Certainly if you fix a particular programming language, that's equivalent to picking a particular logical formalism (and by Gödel's incompleteness theorem we know that can't be the whole story).
But saying that proofs are programs is a more general statement. Computations are always possible to write down as programs, and by the Church-Turing thesis we know that we can pick any reasonably computational model (Turing machines, say, or untyped lambda calculus), and know that we have captured all of them--we don't have to worry about "missing" some extra computations outside the formalism.
The flips side is that without a type system, you can't in general tell which programs are proofs and which are not. But that's as it should be---truth is always an undecidable notion. This means that if we want a foundation for mathematics we should consider _realizability_, not _typeability/provability_ as the most basic notion.
I have no problem with "proofs are programs", only with "programs are proofs", and I think that most of theoretical computer science refuses, almost on principle, to view computation merely as programs expressed in any particular formalism, just as physicists would say that a certain ODE is a description of a falling apple, not that a falling apple is an ODE, nor that an apple can only fall if we can describe it in some formalism.
See the discussion here about realizers vs proofs: https://news.ycombinator.com/item?id=13495547. Perhaps you can shed more light on the subject. Harper's post is interesting, but while it does offer less narrow a view than Wadler's using a different definition of proof (which I don't think deserves the name proof, but nevermind), it is still too narrow a definition of computation (and his introduction of types seems to muddy the water and complicate matters further, partly because the use of types necessitates yet another computation, because types are certificates). Computation is a wider notion than constructive mathematics (as every construction is a computation but not every computation is a construction, and two different computations can yield the same construct).
As to the choice of a foundation of mathematics, I think this is largely an aesthetic matter. It is certainly a separate discussion from computation in the sense that computation does not depend on the choice of mathematical foundation, nor that the choice of mathematical foundation must be built around the notion of computation. I like Turing's view that there are no privileged foundations, and a mathematical formalism should be chosen based on utility, on a case-by-case basis.
