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.
