People certainly have written real software using formal methods: http://compcert.inria.fr/ is a good example.
Of course this does not constitute an argument that programming must be taught as a formal discipline, but it does indicate that formal methods can be useful in some circumstances.
Interestingly, http://compcert.inria.fr/release/Changelog mentions various "bug fixes" in almost every release, and the mentions of "successful tests" are not quite canonical either, but it certainly looks like a successful, nontrivial program.
Yes, CompCert is no timeless perfect gem. You could make a convincing argument that it's not really verified software in the Djikstra mold at all (only parts of the compiler are verified, although they are fairly large and interesting parts).
It does make a nice poster child for formal methods though.
Of course this does not constitute an argument that programming must be taught as a formal discipline, but it does indicate that formal methods can be useful in some circumstances.