Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cs.utexas.edu!uwm.edu!csd4.csd.uwm.edu!markh From: markh@csd4.csd.uwm.edu (Mark William Hopkins) Newsgroups: comp.ai Subject: Re: Reasons why you don't prove your programs are correct Message-ID: <1956@uwm.edu> Date: 18 Jan 90 16:11:03 GMT References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <16479@joshua.athertn.Atherton.COM> <16664@joshua.athertn.Atherton.COM> <1906@uwm.edu> <16692@joshua.athertn.Atherton.COM> Sender: news@uwm.edu Reply-To: markh@csd4.csd.uwm.edu (Mark William Hopkins) Organization: University of Wisconsin-Milwaukee Lines: 34 >markh@csd4.csd.uwm.edu (Mark William Hopkins) writes: >... Some software you can tell will work simply by looking at it -- >that easy they are to prove correct. In article <16692@joshua.athertn.Atherton.COM> joshua@Atherton.COM (Flame Bait) writes: >This is called "looking for bugs" it has nothing to do with proving anything >correct... No, because "looking for bugs" does not involve mathematical proof. This did. It involved proving the program correct, and thus showing that the apparent bug had nothing to do with the program (and therefore with the compiler). In this case, the proof was easy enough that it was not necessary to even write anything down: you could tell just by looking. >"This program is guaranteed to operate consistently with the specifications >outlined in the adjoining document on a CORRECT compiler and operating system. >Any apparent bugs found are solely attributable to one or more of the >utilities used to form the environment of the program." >(the document could be short for all we care, just so long as it specifies >all the details relevant to the user). >I agree that such a proof would be better than nothing. But I have never >seen such a proof for any real world program... ... >Why do you think such a document is possible? Because it will already exist as soon as I finish documentation on a certain "real-world" program. Assembly to boot. The only modifications to the above are the lack of compiler and operating system ... bugs are solely attributable to hardware and circuitry. This circumstance has actually materialised on a few occasions too. So, it exists. The question was never one of existence, but of responsible design.