coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] Axioms reported by coqchk, (continued)
- Re: [Coq-Club] Axioms reported by coqchk, Beta Ziliani, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Pierre Courtieu, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Jacques-Henri Jourdan, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Guillaume Melquiond, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Matthieu Sozeau, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Pierre-Marie Pédrot, 08/19/2016
- RE: [Coq-Club] Axioms reported by coqchk, Soegtrop, Michael, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Jacques-Henri Jourdan, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Pierre Courtieu, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Beta Ziliani, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Guillaume Melquiond, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Robbert Krebbers, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Guillaume Melquiond, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Robbert Krebbers, 08/19/2016
- Re: [Coq-Club] coqchk safe from plugins? (Was: Axioms reported by coqchk), Ralf Jung, 08/19/2016
- Re: [Coq-Club] coqchk safe from plugins? (Was: Axioms reported by coqchk), Robbert Krebbers, 08/19/2016
- Re: [Coq-Club] coqchk safe from plugins? (Was: Axioms reported by coqchk), Jonathan Leivent, 08/19/2016
- Re: [Coq-Club] coqchk safe from plugins? (Was: Axioms reported by coqchk), Robbert Krebbers, 08/19/2016
Archive powered by MHonArc 2.6.18.