🚀 go-pugleaf

>markh@csd4.csd.uwm.edu (Mark William Hopkins) writes:
>...  Some software you can tell will work simply by looking at it --
>that easy they are to prove correct.

In article <16692@joshua.athertn.Atherton.COM> joshua@Atherton.COM (Flame Bait) writes:
>This is called "looking for bugs" it has nothing to do with proving anything
>correct...

No, because "looking for bugs" does not involve mathematical proof.  This
did.  It involved proving the program correct, and thus showing that the
apparent bug had nothing to do with the program (and therefore with
the compiler).  In this case, the proof was easy enough that it was not
necessary to even write anything down: you could tell just by looking.

>"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...
...
>Why do you think such a document is possible?

Because it will already exist as soon as I finish documentation on a certain
"real-world" program.  Assembly to boot.  The only modifications to the
above are the lack of compiler and operating system ... bugs are solely
attributable to hardware and circuitry.  This circumstance has actually
materialised on a few occasions too.

So, it exists.  The question was never one of existence, but of responsible
design.