Where is this strange obsession with Curry-Howard coming from? It's not a practical issue, with regard to verification or otherwise, and the Haskell world in general doesn't try to claim it's one. It's just an interesting symmetry, that's all.
What I mean by that is the philosophy that verification should be based on explicit types in the original program source. This intricately ties the process of authoring software with that of verifying it. The result is needlessly constraining both the developer and the verifier. It only lets you (easily) write code within what it can prove, and only lets you prove properties that can be expressed by the types that you use.
Other approaches say, we'll let people write code however they feel most comfortable doing (more or less), using types whose expressivity is defined not by the limits of the verifier but only by various concerns over language complexity, mental overhead, performance and teamwork, while we let the verifier prove whatever types it can. If it proves that the variable x is of type "an integer which is always equal to the current time in seconds modulo seven, except on Saturdays when it's always zero", then that's great!
I think given your clarification here I can directly state that (a) I don't think this is necessary and (b) I don't think C-H is a good name for this exactly. Point (b) is a bit silly to discuss, but point (a) is key.
I think there are workflow and ux efficiencies for having the compiler reject programs which are poorly typed. This typing can arise from either internal or external verifications for all I care, but the ergonomics of each vary a lot as well.
I think for both practical and ergonomic reasons, completely automated proofs are weak. There's no reason not to run them if you agree with the validity and importance of the theorem they represent, but by their nature the meaning and effectiveness is highly limited.
By having your proving language align with your programming language you sidestep this issue by forcing everyone's hand into revealing their intentions to the verifier. From a process perspective, this keeps people from cheating ("whip and bondage and all that") and it also, more imprtantly encourages the code author to tell a complete story of what they're doing instead of merely creating the artifact. This is great for the more "conversational" style of proving that occurs with things like Agda, Coq, Epigram.
External proofs can act similarly but I think your examples are often really archaic. It seems to me that I nteresting theorems must be derived alongside your program be they internal or external. JonPRL is an interesting demonstration of this method (as is NuPRL, but you can't really access that one).
> forcing everyone's hand into revealing their intentions to the verifier
Only those intentions which the verifier can prove. Want a stronger verifier? You need to change the language.
> encourages the code author to tell a complete story of what they're doing instead of merely creating the artifact
But it's not a complete story. Haskell's type system can't express some of the most interesting bits of the story. I find it ironic that Haskell's type system can't even verify the validity of monads (I mean compliance with the monad laws)...
> External proofs can act similarly but I think your examples are often really archaic.
I don't know if they're archaic, but I do know that Amazon uses TLA+ to verify their Java code (and TLA+ is somewhat similar to Esterel's verifier)
