Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!samsung!xylogics!world!madd
From: madd@world.std.com (jim frost)
Newsgroups: comp.software-eng
Subject: Re: "Program Proving"
Message-ID: <1990Mar20.042134.990@world.std.com>
Date: 20 Mar 90 04:21:34 GMT
References: <52044@microsoft.UUCP> <2480006@hpcuhc.HP.COM> <18190@duke.cs.duke.edu> <1424@oravax.UUCP> <19988@joshua.athertn.Atherton.COM>
Organization: Saber Software
Lines: 17

joshua@athertn.Atherton.COM (Flame Bait) writes:
>I would like to see any of the following four programs verified:
>GnuTar, GCC, GAWK, or G++.

None of these even comes close to passing a good C checker cleanly,
much less a formal proof.  I'd suggest picking something that wouldn't
be so easy to prove incorrect.

The argument is moot, anyway.  Program proving is wonderful when you
absolutely positively must not fail and it's worth the extra time to
do the proof.  For most applications, however, the time necessary to
do the proof would make the application out-of-date before it shipped.
Both sides are right depending on the job requirements.

jim frost
saber software
jimf@saber.com