The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

Hi,

Jason Hickey writes:
 > [...]
 > This seems suprising to me.  Even though the second subgoal is 
 > unprovable, both subgoals are ill-formed.  Is this expected?  Is it 
 > accurate to say that proofs are valid only if one uses the "approved" 
 > functions from the kernel, and one does not use the refiner directly?
 > 
 > Perhaps the Coq semantics ensure that proofs using ill-typed terms are 
 > always invalid.
 > 
 > Peeking inside, we see the following.
 > 
 > proof_type.mli:
 >      and tactic = goal sigma -> (goal list sigma * validation)
 > 
 >      and validation = (proof_tree list -> proof_tree)
 > 
 > These are completely sensible types.  However, is it necessary to make 
 > them public/non-abstract?
 > 
 > I'm not criticizing, I just wonder if I missed something.  We use 
 > similar definitions in MetaPRL, but the tactic and validation types are 
 > abstract outside the kernel.  This helps ensure that correctness depends 
 > only on the kernel/refiner, not on user code (modulo correctness of 
 > OCaml, which is wonderful and reliable).

In  the Coq  architecture, the  correctness is  ensured at  the kernel
level,  once  the  proof  is  completed.   To  be  more  precise,  the
validation above will build the proof  term once the proof is done and
this proof term will be type-checked by the kernel.

Said otherwise, tactics can do anything wrong, it will be caught later
when you  do "Save" at  the end of  the proof. Of course,  tactics are
written carefully  in order  to avoid the  annoyance of a  proof being
rejected at the very end.

This architecture  has a drawback  (basically many things  are checked
twice, though it is possible to use tactics that avoid some checks, as
you did) but the major advantage  that the piece of code to be trusted
is rather small (less than 8% of the code).

Hope this helps,
-- 
Jean-Christophe Filliâtre