I can't answer the question "why I don't prove my programs correct"
because I do.  All the time.  As a matter of course.  Almost without
exception.

As a practical matter, the issues Fetzer raised in his diatribe passing
falsely as a technical article can be largely ignored, both from the
standpoint of engineering and mathematically.  You simply must know
where to draw the line.  You assert a semantics for whatever you can't
prove, assume that as part of your theorey, and proceed.  when you
realize your code, you firewall the parts which are assumed but unproven
with assertions that are executed at run time, and ensure that the
semantics you assumed are the semantics you got.  Thus as a matter of
engineering, Fetzer's Dilemma -- which we might state as "how can
mathematics which is deductive apply to the real world, about which we
can only gather data and validate hypotheses?" -- can be (almost)
ignored.  All the issues raised are issues that apply equally to other
pure vs. applied mathematics dichotomies; all must be handled by the
(implicit or explicit) assumtion that our physical models are a
sufficiently good approximation of the "unspeakable" real world.

But, in fact, these issues had been examined at some length in the
formal methods community.  Had Dr Fetzer been conversant with the
literature, he would have known it; had the reviewers been
appropriately chosen, they would have called him on it.  The fact that
Dr Fetzer's article was published without appropriate examination of
the literature is failure on the part of CACM which I think is very
hard to excuse.

*On the other hand*, Fetzer's Dilemma does expose an unfortunate
tendency in some parts of the formal methods community that we might
term "Hoare's Folly."  Tony Hoare has said in print that proven
programs remove the need to debug *and to test*.  For the reasons that
Fetzer described, this is clearly untrue.  You don't know the way the
apple tastes until you taste the apple.  The program as a mathematical
construct can be proven; the realized program as a physical construct
-- a sequence of executable operations in a physical memory and their
execution in a physical processor -- can AND MUST be tested.

It is a myth that programs must be verified by theorem provers to be
proven.  Hand proofs can be done; in several small experiments I have
seen very large improvements in quality as measured by number of
defects seen per thousand lines of code (I know, I know, but propose a
better measure and I'll use it.)  These are only slightly better than
pure anechdotes; I am currently looking for research funding to perform
experiments which would more strongly confirm the hypothesis.

It is a fact that many of the clients or customers for very highly
trusted programs require verification using a mechanical prover or
proof checker.  I am willing to work with one when it is required, but
there is as yet little evidence that they provide more certainty than
hand proofs, and hand proofs are lots cheaper.  I can't help but think
that the use of theorem provers in this context is often a case of the
old myth that if it's been blessed by a machine, it is somehow ennobled
and incapable of error.

(I'm not claiming that theorem provers are useless, either.  There are
contexts in which they can be very useful.  There is ongoing research
which will help to delimit these contexts.  We need to know more about
it.)

Program proving isn't a panacea: among other things, a proof doesn'
t tell us a damned thing about the suitability of the requirements to
the user's needs.  I don't see how formal methods can help much with
that question, but there is a lot of "requirements engineering"
literature that I should read before I have an informed opinion.

Pant, pant.

These are, of course, only my opinions.  They are not necessarily held
by Duke University, the Department of Computer Science, or any of my
consulting clients, and would probably be bitterly contested by some
subset of the above.
Charlie Martin (c...@cs.duke.edu,mcnc!duke!crm)