The Coq mailing list

[Benjamin Werner <Benjamin.Werner AT inria.fr>]

> 
> This is reasonable, but the new (and weaker) guardedness condition has
> been proved to be consistent, hasn't it?
> 
> So somewhere there *should* a formal study on this... is it accessible?

  Ciao Marino,

You are right, but I have to admit this complete study does not exist
for the moment. The technique to prove normalization and consistency
for a type theory like CIC (I mean with the universes, mutual
inductive types, large elimination, co-inductives, etc) is known but
the time for writing it down properly has not been taken yet...

 Considering however the particular point of guardedness conditions,
it must indeed be said that for the moment these conditions evolve too
fast to hope having the complete proof published or even written down
for the current system before it changes again. Furthermore, the
problems which can occur because of guardedness conditions (linked
with features like mutual inductives a.o.) are typicaly the sort of
things which can easily been overseen in an "informal" proof (I mean
on paper). Finaly, such a study does not prevent errors in the
implementation; again these can occur easily precisely on such
points...

 In other words, this is exactly the kind of problem where you would
like to trust a formal proof. Bruno Barras' work formalizing the
type-checker of Coq in Coq is a hudge step in that respect. On the
particular point of the normalization property we still stumble over
Goedel's incompleteness theorem however.

 I would believe there should be some way around this, in order to
provide reasonable confidence in the formalism *and* the
implementation. But even if we agree on the method, this would in any
case involve a lot of work !


Cheers,


Benjamin