Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!uwm.edu!ux1.cso.uiuc.edu!ux1.cso.uiuc.edu!m.cs.uiuc.edu!p.cs.uiuc.edu!johnson
From: johnson@p.cs.uiuc.edu
Newsgroups: comp.object
Subject: Re: Reasons why you don't prove your pr
Message-ID: <135300020@p.cs.uiuc.edu>
Date: 9 Jan 90 17:38:47 GMT
References: <7578@hubcap.clemson.edu>
Lines: 21
Nf-ID: #R:hubcap.clemson.edu:7578:p.cs.uiuc.edu:135300020:000:1157
Nf-From: p.cs.uiuc.edu!johnson    Jan  8 10:19:00 1990


/* Written  1:22 pm  Jan  7, 1990 by mmm@cup.portal.com in p.cs.uiuc.edu:comp.object */
There was an excellent article about 10 years ago in CACM on this.
I believe the title was "The Social Process and Proofs of Program
Correctness".  This article marked the death of program verification;
feelings which had echoed in the halls of academia and industry
for more than a decade were expressed in a clear form in print,
and from that point on the "conventional wisdom" was that program
verification was a dead-end for research.  In retrospect, it's hard
hard to see why this wasn't obvious from the very beginning.
/* End of text from p.cs.uiuc.edu:comp.object */

Actually, I (and many others) think that the article was full of
half-truths and that its conclusions were generally invalid.  Program
verification is just as popular in academia and industry as it ever
was, and is still receiving government funding.

Now, this doesn't mean that I (or anybody else) actually prove my
programs correct, but the reason is not the ones given in the article
you mention.  Program verification may not yet be practical, but it
is still theoretically interesting.