Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!portal!cup.portal.com!Nagle
From: Nagle@cup.portal.com (John - Nagle)
Newsgroups: comp.ai
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <25728@cup.portal.com>
Date: 8 Jan 90 03:43:08 GMT
References: <7578@hubcap.clemson.edu>
Organization: The Portal System (TM)
Lines: 15


     Manual proofs are worthless (they tend to have bugs, just like programs,
and these bugs usually err in the direction of providing a
false proof) and machine proofs are very hard to do.  See my paper in
ACM POPL '83.  The technology progresses forward by inches, and Don
Good's group at U. Texas has done good work.  Still, all successful
proof efforts that aren't bogus apply to programs of rather modest
size.

     I once headed a group of five people that produced a verifier for
a dialect of Pascal.  It worked, but it was too hard to use to be used
by most programmers.  It's painfully difficult to convince a mechanical
theorem prover that your program is correct.  

					John Nagle