Re: How regularly is the GnuPG source code examined?

From: David Wagner (daw_at_taverner.cs.berkeley.edu)
Date: 09/29/05 

Date: Wed, 28 Sep 2005 22:23:51 +0000 (UTC)

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
>efforts,

Well, I'm not sure this is true -- I think this might be a slight
overstatement.

>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.

Relevant Pages

  • Re: SproutMethod.pdf
    ... > constructing a program such that you can perform even an informal proof ... > of correctness, the quality of design and the correctness of ... If the customer reviews the program, and says, "Okay, move this button ...
    (comp.object)
  • Re: Python from Wise Guys Viewpoint
    ... > myself that it would (in an informal proof type of way), ... > informal proof before moving on, otherwise I'll be beset by gnawing ... For writing my spam filter the process I ... (The whole notion of "correctness" with regards to spam ...
    (comp.lang.lisp)
Quantcast