The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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.

-- Jonathan