[bitc-dev] Type Classes: Pragmatics Questions

[Jonathan S. Shapiro]

On Tue, 2005-08-02 at 11:15 +0200, Dominique Quatravaux wrote:
> I wrote:
> C Y wrote:
> 
> >I'm thinking that you would want the proofs to be human understandable
> >up to the point where the proven system can run a proof checker ;-). [...]
> >  
> >
> >In the end, if I'm understanding this, you have to just trust SOMETHING
> >other than a computer for at least the beginning stages.  
> >
> 
> Well, I believe that mechanical consensus ("the mechanical proof
> verifier whose algorithm is described as text below, validates the proof
> OK when implemented on most computer architectures in most languages")
> is waaaay good enough. Way better anyway than any amount of human
> verification, on proofs of any size and complexity.

I think that this can be reduced to two parts:

1. A credible means to either re-execute or to check the proof. This can
either be a known-good prover, or an independent proof checker, or some
such.

2. A credible set of proof *objectives*. This is the hard part, and it
may still be a place where there is a role for standardization and an
independent evaluation process.

In the end, the purpose of verification is confidence, not perfection.
Concretely, there are three objectives:

1. We would like to build systems where the first cause of unreliability
is failure of silicon, or environmental radiation, or something else
other than software. That is, we would like to improve quality.

2. We would like to establish a new standard of practice for the
construction of critical systems. That is, we would like to increase
expectations.

3. We would like to accomplish these in such a way that the process is
repeatable in an engineering way. If I modify the code, I should not
have to completely re-build my verification from scratch, and I should
have significant automation assistance in re-running the verification.


Item (3) is critical. Unless we can achieve this, verification remains
commercially infeasible and the cost of checkable security and
robustness will remain prohibitive. Unless we can make satisfaction of
requirements checkable by third parties, marketing hype rather than fact
will continue to prevail in the world of secure and robust systems.


Jonathan