The Coq mailing list

[G�rard Huet <Gerard.Huet AT inria.fr>]

I would like to comment on Adam Chilipa's comments, to which I only  
partly subscribe.

True, we want to use the machinery in the best possible computational  
manner, so that most
of proofs are reduced to automatic checking of specifications in some  
ideal tactic language.
If we assume Coq is safe, we may contend with such developments, and  
do not bother anymore about
a human interface to the proof assistant seen as a successful blackbox.

However, here we have two presuppositions. The first one is that the  
automatic proof actually succeeds
on the needed request. Experience shows that this is rarely the case,  
and that manual steps by a knowledgeable
user of the system are needed to conclude the proof. Hence debugging  
is essential, and reverse-engineering
of diagnostic messages demands a close adequation with a human- 
readable sentence of the description of some current proof
contextual object. Whence the need for names and other more or less  
dynamic notations necessary to communicate
the current state of the proof search to the original human client.

The second presupposition is that Coq is safe. Actually, whatever we  
may think of the absolute safeness of such version of Coq,
the relevant question rather is: Should Coq be trusted ? Coq cannot  
be trusted just on statements from the developing team
or vague belief in some trustable academic publication plus reliance  
on expertise of the software developing team.
Trust comes from judgement from an independent entity, namely a  
certification agency. The certification agency is there
to give an official seal of approval to the formal developments  
required from some quality evaluation regulation.
At present, the requirement is that the formal proof ought to be  
readable and understandable by a human auditor,
which by the way makes sense even for gigantic proofs by statistical  
sampling.
So if the real software system we are talking concerns a safety- 
critical application, then yes, the human-readable
proof with the damned names and everything is needed, if you need  
your product to be certified for security.

The other point on which I disagree is that the proof of real  
applicative systems is necessarily a mess.
Software design will slowly pull us out of this morass of bugs and  
hopefully some day reach the quality achieved
in hardware design.

This does not diminish the interest of automated proofs on well- 
designed tactic notations, on the contrary.

Gérard Huet

Le 31 août 07 à 20:20, Adam Chlipala a écrit :

> Stefan Monnier wrote:
> > The problem I have with separate lemmas is that it forces you to  
> > write the
> > whole statement (i.e. type) of the lemma, which may be large and is
> > otherwise automatically computed/inferred by Coq.
>
> Even that forces you to know the order in which the inductive cases  
> are generated, to match cases with names in a sensible way.  My  
> personal preference is for working toward automating all proofs,  
> meaning not using any tactics that refer to variables/hypotheses by  
> name, except for initial 'induction' invocations and similar.  This  
> obviously doesn't lead to readable proof argument that tell "why" a  
> theorem is true, but I'm very skeptical that such arguments will  
> ever exist for proofs about real software systems, for instance.   
> Thus, I think it makes sense to focus just on establishing that  
> theorems hold and leave the "readable" step-by-step proofs for  
> results simple enough to fit in a conference paper in informal form  
> (in other words, not proofs about real systems!).
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club