The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> To be clear - are people suggesting that if axioms in the standard
> libraries are placed in separate modules, then they don't believe a tool
> that can check the actual dependency of a development on axioms is
> desirable?
> 
> This means they are placing considerable trust that a standard library
> module that is not supposed to have an axiom stays that way. They are
> also placing similar trust in any user-developed modules they use. 
> Consider how easy it is to create something in Coq that is an axiom
> without using Axiom - one merely needs a top-level Variable, Context, etc.
> 
> Such trust in a module's claim not to involve axioms seems to me to not
> be within the spirit of Coq: small kernel, coqchk that doesn't load
> plugins - both of which (especially when compared to what Coq's
> competitors provide) enhance Coq's trustworthiness.

We'd only "trust" those libraries insofar as, if they fail to behave,
we'd get coqchk reporting axioms even though we don't use any.  So, that
"trust" is not part of the TCB.  I don't see how this violates or is
even related to the usual Coq trust assumptions.

I'd love to see coqchk become smarter here.  I just had the impression
that the Coq developers are reluctant to add such complexity to coqchk.

Kind regards,
Ralf