Just a note for those who find "The Future of Programming" advogato post interesting: you might have a look at the book "High Integrity Ada" by John Barnes (Addison-Wesley), it describes a safe "provable" subset of Ada 95 known as "SPARK 95". Also look at the message of Peter Amey in the thread "High integrity software" of the comp.lang.ada newsgroup for some interesting claims.
Formal proofs are in use today with existing languages for non-trivial software, it's just not C/C++ (as the cvsup author John D. Polstra wrote it's "notC" ;-) and what can be called a typical hacker environment and mindset. Needless to say I regret this a lot, in particular the Ada entry of the Hacker's dictionary is highly misinformed ;-).
As for proving with C, it's uselessly hard because the pointer model is pervasive. And for the C++ template model, AFAIK, it does not even enforce interface and implementation separation which is quite essential for scaling up (you need to know all the implementation code to see if your template use will work).