🚀 go-pugleaf

In article  <12297@dog.ee.lbl.gov> Chris Torek writes:
]>In article <1726@optima.cs.arizona.edu> gudeman@cs.arizona.edu
]>(David Gudeman) writes:
]>>Finally, consider the relationship of the proof to the real world ...
]>>you will have to deal with the philosophy of mathematical models.
]
](This goes well off the beam of comp.lang.misc.  You must also deal
]with the question of objective reality, and whether, if it exists at
]all, it can be perceived.

eek.  I wasn't going that far out.

]Likewise---and perhaps this is what David Gudeman is talking about---we
]can use mathematical models of computer behaviour quite effectively,
]but we should keep in mind that they are only models.

Exactly one of the points I wanted to make.  Models are by their very
nature abstractions, and abstractions by their very nature leave out
some details.  You have to remember that your theorems are only true
if you stay within the limits of the abstraction.

]My own position on this is that both methods should be used in
]moderation, and in proportion to the importance of the problem.

That is my position on the question of whether formal program
verification is "useful" -- it certainly is.  But I wanted to get at
something about the nature of program verification, where I think
people have mistaken ideas.

Part of the mistake comes from the term "proof of correctness".  What
does such a proof really prove (assuming that the proof is correct in
the first place)?  First, I will point out what it does _not_ prove:
it does not prove that the program actually behaves in the way that it
is expected to.  That is the point that I think a lot of people are
missing.  So what does it prove?  Given a program P1 in programming
language L1 with formal semantics M1; and a formal specification P2 in
specification language L2, with formal semantics M2; a formal proof of
correctness of L1 is just a proof that the meaning of P1 under the
semantics M1 is the same as the meaning of P2 under the semantics M2
(where "is the same as" has some formal meaning that varies according
to the proof technique).

Now, what does such a proof tell us about the real-world question of
whether the program P1 behaves as we want it to?  Nothing.  It tells
us that P1 behaves as P2 says it will.  How do we know that P2
specifies that P1 will behave as we want it to?  We don't.  We _can_
say that if our confidence in P2 was greater than our confidence in
P1, then (assuming we have complete confidence in the proof itself)
the result of the proof is that our confidence in P1 is now the same
as our confidence in P2.  But the problem is that there is no a priori
reason that our confidence in P2 should have been higher than P1.

But let us assume that such a reason exists.  Possibly P2 is much
shorter than P1 because it is in a higher-level language or because
the paradigm of L2 is more suited to the problem than is the paradigm
of L1.  But if that is the case, then why not just write the program
in L2 in the first place?  One could answer by saying that L2 is too
inefficient for a programming language.  Fine.  Then let's not pretend
that our "proof of correctness" is a way to prove a program correct;
it is just a way to prove that an efficiency hack preserves the
semantics of the program (where the "efficiency hack" is to recode the
inefficient program P2 in the more efficient language L1).

Many people claim that we have more confidence in P2 than P1 just
because L2 is a "mathematical" language.  I don't think there is any
basis for such a distinction unless P1 is designed to be a low-level
implementaton language.  In such a case I say that P2 should be the
programming language and recoding in P1, again, is just an efficiency
hack.

Just because L1 uses the paradigm of imperative procedures and L2 uses
the paradigm of predicate logic, is no reason to say that P2 is more
reliable.  I think people who argue that predicate logic is a "better"
notation than imperative procedures are deceived in thinking that
imperative procedures inherently have the messy, low-level semantic
nature they have in many real programming languages.  But is isn't
fair to compare C to formal predicate calculus.  A better comparison
is Lisp to Prolog.  Both are general-purpose programming languages at
about the same "semantic level", and they are equally good (or bad)
for formal purposes.

So why do I still think formal verification is a good idea?  Given two
different programs P1 and P2 to solve the same problem, it seems
reasonable to assume that the probability that the programs both have
an identical error is small compared to the probability that each
might have an arbitrary error.  Given a proof that the two programs
are "the same", we know that any errors that either one has, it has in
common with the other one.  We have already said that such a
probability is smaller than the probability of individual errors, so
we have increased our confidence.  You could formalize this in
probability theory to find out how much confidence we need in the
proof and how much lower the probability of mutual errors has to be
for the level of confidence to increase.  Any takers?

You can informally decrease the probability that two different program
will have identical errors by writing them in different programming
languages.  You can further decrease the probability by using two
languages with radically different paradigms (which is the usual
verification technique).  Even better would be to have different
programmers do the work in different languages with radically
different paradigms.  Of course once this is all done, you still don't
know if the thing runs until you test it.  You can still run into
compiler bugs.

So the answer to my original question: "What do you know after a
formal proof that you did not know before the proof?" is "You know
that the program implements the formal specification.  You don't
formally 'know' anything more about the program's real behavior than
you did before."
--
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman