The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 19/08/2016 16:39, Ralf Jung wrote:
> If the answer is "yes", then being able to filter things in coqchk
> becomes less pressing.  There's still the concern of libraries not
> following this policy to the letter and having axiom-free useful stuff
> in an "axiom-infected" module; maybe that's sometimes just easier to
> structure.

As a personal stance, I think we should keep coqchk as dumb as possible,
as this reduces the TCB (Print Assumptions is already fishy enough not
to include it in the checker). Conversely, we should do our best to
provide axiom-free tools and rely on axioms in an opt-in fashion.

Axioms are bad™. Remember the dreaded PropExt soundness!

PMP

Attachment: signature.asc
Description: OpenPGP digital signature