Re: How regularly is the GnuPG source code examined?
From: Jon A. Solworth (solworth_at_cs.uic.edu)
Date: Fri, 14 Oct 2005 07:12:59 -0500 To: David Wagner <firstname.lastname@example.org>
Interesting discussion, and I'm certainly not disagreeing
with Vernon or David here. But I think the problem with formal
verification is the term itself---its misleading. The techniques
would be more accurately called "formal assurance".
(It is not even that "formal verification" is wrong in an ordinary
english [rather than technical vocabulary] sense. There
are two senses of verification: one is truth and the other is evidence
in a legal sense of evidence. Just as it would be misleading to use
the term "proof" in a formal mathematical setting to talk about legal
proof rather than mathematical proof.)
David Wagner wrote:
> Vernon Schryver wrote:
>>It is not merely that full mechanical proofs of correctness have never
>>been demonstrated except for trivial cases, and then only with heroic
> Well, I'm not sure this is true -- I think this might be a slight
>>verification cannot do more than relate the program
>>to some other specification.
> Right, I agree, this is a key issue that is often overlooked. First,
> you have to know that your specification is correct (it is the spec
> you wanted). Also, you have to make sure that all the assumptions made
> during verification are valid (e.g., that your CPU correctly implements
> the instruction set; that your compiler correctly compiles the source
> language; and so on).
> But, as both you and Brian Gladman have written, formal verification is
> still useful despite these significant limitations.
>>Competent programmers write with proofs of correctness in mind. Any
>>code that does not have an informal proof of correctness obvious from
>>the source or from comments is dubious. That proof will be as informal
>>as proof of a mathematical statement.
> Right. This is often a very helpful way to structure your thinking
> about code, even if you never touch a theorem prover or write down the
> argument in any formal way. For instance, loop invariants are a useful
> concept even if the code is never formally verified in any way.
>>Just as errors will always be found in published proofs, there will
>>always be bugs in code. The tools of various sorts of verification
>>can significantly reduce those errors, but never eliminate them.
> Right. Significantly reducing the incidence of errors, and eliminating
> certain sources of errors, is useful, but it isn't going to bring us to
> zero defects.
> I guess I'm in violent agreement with most everything you say.