Xref: utzoo comp.ai:5394 comp.arch:13027 comp.databases:4554 comp.edu:2872 comp.object:685
Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!samsung!usc!apple!fox!portal!cup.portal.com!mmm
From: mmm@cup.portal.com (Mark Robert Thorson)
Newsgroups: comp.ai,comp.arch,comp.databases,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <25711@cup.portal.com>
Date: 7 Jan 90 19:22:24 GMT
References: <7578@hubcap.clemson.edu>
Organization: The Portal System (TM)
Lines: 8

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.