Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Axioms reported by coqchk

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Axioms reported by coqchk


Chronological Thread 
  • From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Axioms reported by coqchk
  • Date: Fri, 19 Aug 2016 16:49:57 +0200

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




Archive powered by MHonArc 2.6.18.

Top of Page