# Re: How regularly is the GnuPG source code examined?

**From:** Jon A. Solworth (*solworth_at_cs.uic.edu*)

**Date:** 10/14/05

**Next message:**tomstdenis_at_gmail.com: "Re: How regularly is the GnuPG source code examined?"**Previous message:**O.L.: "Re: Symetric encryption : DES or not DES ?"**Next in thread:**tomstdenis_at_gmail.com: "Re: How regularly is the GnuPG source code examined?"**Reply:**tomstdenis_at_gmail.com: "Re: How regularly is the GnuPG source code examined?"**Maybe reply:**D. J. Bernstein: "Re: How regularly is the GnuPG source code examined?"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

Date: Fri, 14 Oct 2005 07:12:59 -0500 To: David Wagner <daw-usenet@taverner.cs.berkeley.edu>

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

Jon

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
*

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

**Next message:**tomstdenis_at_gmail.com: "Re: How regularly is the GnuPG source code examined?"**Previous message:**O.L.: "Re: Symetric encryption : DES or not DES ?"**Next in thread:**tomstdenis_at_gmail.com: "Re: How regularly is the GnuPG source code examined?"**Reply:**tomstdenis_at_gmail.com: "Re: How regularly is the GnuPG source code examined?"**Maybe reply:**D. J. Bernstein: "Re: How regularly is the GnuPG source code examined?"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]