🚀 go-pugleaf

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.
    <Put most any real world program here>

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