Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!umich!samsung!zaphod.mps.ohio-state.edu!tut.cis.ohio-state.edu!ucbvax!hplabs!nsc!pyramid!athertn!joshua From: joshua@athertn.Atherton.COM (Flame Bait) Newsgroups: comp.ai Subject: Re: Reasons why you don't prove your programs are correct Message-ID: <16692@joshua.athertn.Atherton.COM> Date: 17 Jan 90 02:01:50 GMT References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <16479@joshua.athertn.Atherton.COM> <16664@joshua.athertn.Atherton.COM> <1906@uwm.edu> Reply-To: joshua@Atherton.COM (Flame Bait) Organization: Atherton Technology, Sunnyvale, CA Lines: 48 markh@csd4.csd.uwm.edu (Mark William Hopkins) writes: >It's funny, because a student once came to me with a 200-300 line Pascal >program, trying to figure out what was wrong with it. I looked at it in >detail, and simply by inspection could tell her that there was nothing wrong >with it. Some software you can tell will work simply by looking at it -- >that easy they are to prove correct. This is called "looking for bugs" it has nothing to do with proving anything correct. I think it was Nagel who said that proofs done by hand tend to have just as many bugs as the programs they describe, and the bugs tend to falsely imply that the program works, or very similar words. >The mentality was so ingrained in people (which was actually picked up from >the course) that programs are creatures to be analysed behaviorally, instead >of mathematical constructs, that it simply never occurred to this person that >she might be able to prove that the fault did not lie with her program. This might be true in general, but not me. My profs tried hard to convince me that programs are just mathamatical constructs, and could be proven just like geometry. A lot of people who teach about software, but do not write it commercially seem to think this. I think that programs are much more like biological organisms than mathmatical constructs. For example, mathmatical constructs are static over time, but organisms and programs change over time. Mathmatical constructs can not learn, but animals can learn, and programs tend to "learn" their test suites. (That last bit is a quote from a friend of mine, which has proven very true. It is not exactly like animal learning, but it is similar.) >A program verification would look like this: >"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. One of the important parts of my argument is that the document which you so easily assumed (just like the economist of my previous posting) can not exist. Show me a machine readable specification for the compiler, linker, loader, or assember which is useful in program verification for any major operating system. Why do you think such a document is possible? Joshua Levy (joshua@atherton.com)