I agree that it is good separate programming and verification. Otherwise the programmer is forced by the compiler to worry about correctness and termination from Day 1.

Moreover, Cury-Howard based approaches really work only for a restricted form of programming: pure and total functions.