Program verification is not a silver bullet
Alan Shostack points out that
Alan Drexler is excited about the interesting AMS survey article
“Formal Proof” (Hales)
because of the prospects for program verification.
I think the article is better at inspiring hope about computer verification of proofs than about proof system verification of computers.
For balance one should read the still-persuasive May 1979 paper
“Social processes and proofs of theorems and programs” (De Millo, Lipton, Perlis).
The abstract:
It is argued that formal verifications of programs, no matter how obtained, will not play the same key role in the development of computer science and software engineering as proofs do in mathematics. Furthermore the absence of continuity, the inevitability of change, and the complexity of specification of significantly many real programs make the formal verification process difficult to justify and manage. It is felt that ease of formal verification should not dominate program language design.
(Note that that there are lots of copies cached around the web if you don’t have an ACM Portal subscription.)
