Xref: utzoo comp.ai:5552 comp.edu:2914 comp.object:745 Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!samsung!usc!apple!oliveb!pyramid!athertn!joshua From: joshua@athertn.Atherton.COM (Flame Bait) Newsgroups: comp.ai,comp.edu,comp.object Subject: Re: Reasons why you don't prove your programs are correct Message-ID: <16664@joshua.athertn.Atherton.COM> Date: 15 Jan 90 18:41:00 GMT References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <16479@joshua.athertn.Atherton.COM> Reply-To: joshua@Atherton.COM (Flame Bait) Organization: Atherton Technology, Sunnyvale, CA Lines: 37 kers@hplb.hpl.hp.com (Kers) writes: >I'll also think that the remark "specifying most programs is impossible" is >wrong. "bloody difficult, especially after the fact" is the predicate that >springs to mind. No problem. Specifiy the following programs, in a machine readable format useful to a program verifier. These should be commerical products, so they must look good and feel good so that people want to use them: A rule based expert system shell. Remember to specify input and output for an window based system. A source code control facility like SCCS or RCS If you use system calls you must have some way of proving that they do what your spec says they do. My last example points out a current problem with proving program correct. They must only use libraries which have been proven correct, must run on an operating system which has been proven correct, and must use hardware which is proven correct. All of this is impossible right now. I'm serious about this challenge. I hold that these program can not be specified in any kind of useful way, and that the set of programs which can be proven correct is so small as to be uninteresting. I assume everyone has heard the joke about three people (a chemist, a physist, and an economist) who are trapped on a desert island with only cans of food. The punch line is the economist saying "Imagine a can opener". I often think of this branch of the "software proof" camp in the same way. As long as they stick to mathmatical programs which do not have input, output, or any other real life constraints, they can create interesting examples. Joshua Levy joshua@atherton.com home:(415)968-3718 {decwrl|sun|hpda}!athertn!joshua work:(408)734-9822