🚀 go-pugleaf

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)