A nice counterpoint to de Millo, Lipton, and Perlis

Asperti, Geuvers,and Natarajan have this fun paper, Social processes, program verification, and all that, which provides a nice counterpoint to the 1979 De Millo, Lipton, and Perlis which supposedly killed the verification effort at the time. The De Millo paper argues that because proofs are social processes verified by the intuition of mathematicians, mechanized verification is a useless effort.

My favorite quote from the De Millo paper:
The verification of even a puny program can run into dozens of pages, and there's not a light moment or a spark of wit on any of those pages. Nobody is going to run into a friend's office with a program verification. Nobody is going to sketch a verification out on a paper napkin. Nobody is going to buttonhole a colleague into listening to a verification. Nobody is ever going to read it. One can feel one's eyes glaze over at the very thought.

From this paper:
As we have already observed, the gloomy predictions of De Millo et al. have been largely refuted. Formal verification is at present a concrete reality, permitting correctness proofs of complex software applications. For instance, in the framework of the Verifix Project a compiler from a subset of Common Lisp to Transputer code was formally checked in PVS (see Dold and Vialard (2001)). Strecker (Strecker 1998) and Klein (Klein 2005) certified bytecode compilers from a subset of Java to a subset of the Java Virtual Machine in Isabelle. In the same system, Leinenbach (Leinenbach et al. 2005) formally verified a compiler from a subset of C to a DLX assembly code. The Compcert project, headed by Xavier Leroy, has recently produced a verified optimising compiler from C to PowerPC assembly code, based on the use of the Coq proof assistant both for programming the compiler and proving its correctness (Leroy 2006; Tristan and Leroy 2008). Similar achievements have been obtained in other fields of computer science, spanning the range from hardware (Harrison 2007) to operating systems (Alkassar et al. 2009; Klein 2009).