Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!usc!brutus.cs.uiuc.edu!ux1.cso.uiuc.edu!ux1.cso.uiuc.edu!m.cs.uiuc.edu!render
From: render@m.cs.uiuc.edu
Newsgroups: comp.software-eng
Subject: Re: "Program Proving"
Message-ID: <39400077@m.cs.uiuc.edu>
Date: 7 Mar 90 01:39:46 GMT
References: <52044@microsoft.UUCP>
Lines: 33
Nf-ID: #R:microsoft.UUCP:52044:m.cs.uiuc.edu:39400077:000:1712
Nf-From: m.cs.uiuc.edu!render    Mar  6 10:19:00 1990


Written  1:31 pm  Mar  5, 1990 by jimad@microsoft.UUCP:
>For the record, the last time these flames flared up a month or two ago,
>I asked for any authors with a "proven correct" non-trivial program that 
>they were willing to submit for critique --said program written in C 
>and runnable on a PC-- to submit such for my edification.
>
>I received no such "proven correct" programs.

For the record, I told you about the development of a version control
system based on formal development techniques.  Because I didn't work
on the project, I don't have the code, so I can't send it to you.  Still,
given the article there is a strong likelihood that such a program does 
exist and was proven correct by your standards.  I've included the reference
again at the end of this note.  You should try to contact the people involved
to see what happened to the code.

Speaking of "your standards", what is the point that you're trying to make?
That no such programs exist?  So far as I know they do, although I am not
involved in the area and only hear about such work second- and third-hand.
Still, even if no non-trivial programs have ever been verified, it would 
not indicate that program verification research is a waste of time.  Indeed,
the work would be even more important so that we can determine exactly why 
programs are hard to verify and see if it is a fundamentally intractable 
problem.  Hand-wavy arguments are not good enough, at least if you want
to call yourself a computer scientist or a software engineer.

hal.
----

 Ian D. Cottam, "The Rigorous Development of a System Version Control Program",
    _IEEE Transactions on Software Engineering_, vol. SE-10, no. 2, March 1984,
    pp. 143--154.