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 <dawusenet@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 itselfits 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 ]
Relevant Pages
