Theorem provers might be slow and expensive, but program provers are
   not available at any seed or price.  Indeed it is doubtful that such
   programs can be written at all.  (See the CACM article entitled "
   Program Verification: The Very Idea".  I can no longer remember the
   exact CACM it was in, sorry.  My best guess would be Sept. 1986 or 1989.)

This article is only of interest because of the resulting CACM Flame-Fest
that ensued.  The article itself merely makes the obvious statement that
a program-proof is wrt some set of axioms about the behaviour of the hardware
that the program runs on.  The article's author then concludes that you "cannot
prove programs correct" because the hardware may not satisfy the axioms.
Personally, I would be very happy with a program that would only malfunction
if the hardware adds 1+1 and comes up with 3.

What the author (and apparently the poster) fails to realize is that the
purpose of a program proof in the real world is to increase your confidence
that the program will do what you want it to do.  Sure, some academics with
axes to grind (and grants to obtain, and tenure to achieve) indulge in some
faulty advertising, but anyone seriously working in the area is aware that
a proven program can still fail to do what the user wants it to do.

Of course the hardware axioms could
be unsatisfied, the proof itself could be faulty, a faulty compiler could be
used, etc., but that does not eliminate the fact that a program proof
increases your confidence that the program does what you want it to do.

   As was discussed in another new group (comp.ai or comp.object), assertions
   have little to do with proving a program correct.  The best they can
   do is prove that the assertions are met.  While this is a good thing,
   it does not PROVE anything.  How do you prove that the assertions assert
   anything useful?

This comment applies to any technique that can be used to increase your
confidence in a program, and is totally pointless.  To repeat, the point of
a program proof is to increase your confidence that the program does what
you want.  Neither it, nor any other technique will guarantee it.  Sometimes
testing is better, sometimes code walkthroughs, usually a combination of
all the various techniques is best.

Geoff Clemm