Xref: utzoo comp.ai:5603 comp.edu:2934 comp.object:765
Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!uwm.edu!bionet!ames!sun-barr!ccut!titcca!kddlab!icot32!hawley
From: hawley@icot32.icot.jp (David John Hawley)
Newsgroups: comp.ai,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <6121@icot32.icot.jp>
Date: 18 Jan 90 01:19:12 GMT
References: <16479@joshua.athertn.Atherton.COM> <1455@krafla.rhi.hi.is> <16665@joshua.athertn.Atherton.COM> <10289@microsoft.UUCP>
Reply-To: hawley@icot31.icot.junet (David John Hawley)
Followup-To: comp.ai
Organization: Fifth Generation Computing Systems (ICOT), Tokyo, Japan
Lines: 25

In article <10289@microsoft.UUCP> you write:
>...
>The way one discovers bugs in one's software is not by trying to prove its
>correct, but rather by trying to show it is incorrect, and how.  Trying to
>'prove' software is correct does nothing to improve the quality of the software
>involved.  Finding and removing bugs does.  The trick is to try to find
>and fix as many bugs as cheaply as possible in a reasonable amount of time.
>Is a new, high quality car free of bugs?  NO -- it has hundreds or thousands
>of engineering and manufacturing imperfections.  Likewise any reasonably
>sized piece of software...

I think this analogy is misguided. The proper analogy with manufacturing and
software would be that the manufacturing process (software) has flaws and
these result in unacceptably high-levels of flawed goods (output).  It is
important to note that there is one process and multiple instances of its
output. It seems more efficient to fix the process than fix each output item. 
It's maybe even better to design the process the right way in the first place.

Actually I agree with what has been said in this newsgroup about concentration
on formal specifications obscuring the real problem which is modelling the
real world, but it is also nice to know that your models are faithfully
represented in your experiments (programs).

Returning to the article quoted above, since the analogy is bad I can't see
any merit in the conclusions.