🚀 go-pugleaf

In article <16664@joshua.athertn.Atherton.COM> joshua@Atherton.COM (Flame Bait) writes:
>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.

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).

Just because a program may be operating in a faulty environment does not mean
that verification cannot be done with it.  Verification is ALWAYS done
conditionally on the assumption that everything being used to support the
software is correct.  In this context, it's only purpose is to eliminate the
sources of possible bugs (it can't be the software, so it must be the
firmware or even the hardware(!)).  And by verification I DO mean mathematical
verification.  Of course, you will do some actual run-time testing whose
purpose is to aid in the discovery of the mathematical properties of the
software.  That way you can significantly automate much of the discovery
process.

That's how I've been able to detect bugs in system utilities, such as a
local Pascal compiler, an assembler, and even circuitry quite a few times.
Never managed to find fault with a chip yet though...

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.

So ... it was the compiler.

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.

>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.  

The irony...