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

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