Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!swrinde!elroy.jpl.nasa.gov!ncar!noao!arizona!gudeman
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <1755@optima.cs.arizona.edu>
Date: 11 Apr 91 19:17:30 GMT
Sender: news@cs.arizona.edu
Lines: 61

In article  <1991Apr11.161347.26513@watmath.waterloo.edu> Michael Coffin writes:
]In article <1726@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
]>Can anyone who thinks it is useful to "prove" programs correct provide
]>me with an explanation of exactly what the proof accomplishes?  What
]>do you know after the proof that you didn't know before the proof?...
]
]If I prove a program correct I have a high degree of confidence that
]the program will work.  If I both prove it and test it my confidence
]is extremely high.  Even then I'm not *certain* that it will work.

I will accept that, but it isn't really what I was getting at.  What I
meant is this: you have a programming language which is a formal
notation, and you have written a program in that notation that you
believe accomplishes some goal.  You also have a mathematical notation
in which you can prove the "correctness" of the program in the
programming language notation.  Now I have the following questions:

(1) given that you already think the program is correct by the rules
of its own notation, why does it increase your confidence just because
you have another "program" in another notation that says the first one
is correct?

(2) Is the mathematical notation more reliable in some sense?  If so,
how?

(3) Is formalism (proof of correctness) more reliable than experience
(testing)?  If so, how?

I would answer that yes, proofs of correctness do increase the
confidence in a program, but not because of (2) or (3), to which I
would answer "no".  There is another reason that proofs of correctness
are useful that I think Mike knows but hasn't expressed clearly.
Hint: what is the main way to acheive fault tolerance?

]Why do you set proofs against testing?  Why not do whichever is
]appropriate, or do both?  For code that counts the lines in a file,
]testing is fine.  For a distributed program that flys an airplane or
]monitors my vital signs, both testing and proof are appropriate.

Absolutely, I don't think we disagree on this point.  My complaint is
with people who think that proofs of correctness are some form of
magic that give supreme confidence in a piece of software, and that
testing is just a dubious hack.  In fact, (and this is where
philosophy comes in) any confidence we might have in formalism rests
ultimately on experience.  I see no basis to put this sort of
generalized, historical experience at a higher level of reliability
than direct experience.

]Also, I don't understand the parenthetical comment.  You *can* test a
]proof by independently deriving another.

The point is that just because a proof proves something that happens
to be true, that doesn't mean the proof is correct.  The proof can
have errors that act together in such a way to still give the correct
result.  If you independently derive another proof, you have increased
confidence that the _theorem_ is correct, but I don't think it has as
big an effect on showing that the original _proof_ was correct.
--
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman