I agree that this is only true when the language is given a strong enough type and that giving such a type may be to cumbersome. In fact languages that can do most of these things already exist (Coq and Agda for example) but they are indeed to cumbersome.
That is why we need people experimenting with new languages like Epigram, attempting to find a way of writing these programs in such a way that these strong types don't become to cumbersome.
These strong types will always be somewhat cumbersome, because they are the proof that your program is correct in certain respects, and non-trivial proofs are not free. When you hear someone use the phrase "correct by construction," you should ask you do when you accidentally construct the wrong thing. I'm afraid the answer is that you "correct by reconstruction."
That is why we need people experimenting with new languages like Epigram, attempting to find a way of writing these programs in such a way that these strong types don't become to cumbersome.