Path: utzoo!censor!geac!torsqnt!lethe!yunexus!ists!helios.physics.utoronto.ca!news-server.csri.toronto.edu!cs.utexas.edu!uunet!microsoft!jimad
From: jimad@microsoft.UUCP (Jim ADCOCK)
Newsgroups: comp.software-eng
Subject: Re: Proofs (was: Global program state.)
Message-ID: <70046@microsoft.UUCP>
Date: 15 Jan 91 19:00:33 GMT
References: <2474@motcsd.csd.mot.com| <10370@lanl.gov> <1070@tetrauk.UUCP> <1987@oravax.UUCP> <1991Jan11.175952.10978@pdn.paradyne.com>
Reply-To: jimad@microsoft.UUCP (Jim ADCOCK)
Organization: Microsoft Corp., Redmond WA
Lines: 16

In article <1991Jan11.175952.10978@pdn.paradyne.com| locke@nike.paradyne.com (Richard Locke) writes:
|[not redirection from discussion in comp.object]
|
|Capers Jones makes the interesting statement that there isn't any
|empirical evidence that correctness proofs are an effective defect
|removal or defect prevention strategy (in the context of "real"
|product development efforts).
|
|Does anyone have evidence to dispute this?

Not disputing this -- but another data point:  A while back I asked on
notes for any "non-trivial" program examples from the "proving" camp
that I could compile and execute on a PC [since this is my development
environment], for my own edification, and I volunteered to report back to
the net what I found.  ["Non-trivial" was to be defined by the program-
submitter.]  I received no offers.