Xref: utzoo comp.ai:5576 comp.edu:2921 comp.object:751
Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!microsoft!jimad
From: jimad@microsoft.UUCP (JAMES ADCOCK)
Newsgroups: comp.ai,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <10289@microsoft.UUCP>
Date: 16 Jan 90 18:15:21 GMT
References: <16479@joshua.athertn.Atherton.COM> <1455@krafla.rhi.hi.is> <16665@joshua.athertn.Atherton.COM>
Reply-To: jimad@microsoft.UUCP (JAMES ADCOCK)
Organization: Microsoft Corp., Redmond WA
Lines: 32

Given that real-world commercial software products of typical size have
thousands, if not tens-of-thousands of bugs discovered before shipping,
and that most of those bugs have to be fixed, and a few passed over,
it seems that one would be better off *not* trying to prove that
your [non-trivial] piece of code is correct, but rather understanding
when a piece of code fails, under what conditions, and make sure you have 
the most important day-to-day situations covered.

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.  Rather than try to 'prove' your auto is
perfect, better to test that the wheels don't all fall off while driving
down the freeway at 60 miles an hour.

Again: 'proving' that software is correct does nothing to improve the
quality of that software.  Finding and removing bugs does improve the
quality of software.  Find and remove the worst bugs as cheaply as 
possible in order to create the highest quality of software you can produce.
The cheapest bug to remove is the one that was never introduced.  And you 
can't introduce bugs in code never written.  So only write code for the
most needed features.  And make sure you wring most of the bugs out of
those features.  

The proper approach to quality software has more to do with Shewhart 
and Deming than Turing.

Standard disclaimer.