At POPL someone asked after some verification talk what was different about this current wave of hype regarding machine-checked proofs of correctness. The speaker discussed how we have developed better proof techniques and our machines have gotten a heck of a lot faster, so maybe this time verification is here to stay. I have been thinking a lot about the question of whether verification is here to stay and why. While I buy the "machines are faster argument," I still think a lot about the role of verification in our daily lives.
Something interesting to think about is the proofs as social processes paper which supposedly killed verification for a bunch of years. This paper says that because proofs are not meant to be completely formal and only meant to be discussed among mathematicians, machine checked proofs are not going to do anything for us. While de Millo makes a good point that verification still doesn't tell us about some absolute notion of correctness, his tone is very extreme and there seem to be many red herrings. (For instance, he uses Rabin's pseudoprimes as an analogy for the concept that we should regard mathematical proofs as "probably correct.") Also, one of the main points seem to be that verification will not go anywhere because the proofs are too long and ugly he doesn't address the counterargument that maybe mathematicians have been doing it the other way because machine proof techniques were not good enough.
This paper generated some interesting discussion at the last Software Design Group tea, which I sometimes crash. There were extremes of opinion: while some people thought the paper was well-crafted and prescient, there were others who were so angry with the argument and the manner in which it was made they were ready to physically defend their principles. At this tea I learned that the de Millo paper was targetting the views of those like Dijkstra, who believed in a notion of ultimate correctness. Dijkstra wrote a colorful rebuttal comparing the de Millo paper to a "political pamphlet from the Middle Ages"--also a good read. ;)