The Coq mailing list

["Ade Umut Huxtable" <tkdtezx AT mail.nu>]

The question is,
- do you use a simple tool like coqchk, which looks through all referred 
modules, and reports any axioms found, regardless whether your theories 
actually use it or not
- do we need a new tool, which is cleverer than coqchk, and only reports 
axioms actually used (like Print Assumptions.), but pay for this with 
increased complexity (thus more bugs, unless the tool itself is written in 
Coq :) ).

If libraries would split up, we could use the simple tool, to ensure our 
development uses no axioms/only uses the axioms we expect.

--- 
pierre.courtieu AT gmail.com
 wrote:

From: Pierre Courtieu 
<pierre.courtieu AT gmail.com>
To: Coq Club 
<coq-club AT inria.fr>
Subject: Re: [Coq-Club] Axioms reported by coqchk
Date: Mon, 22 Aug 2016 00:14:17 +0200

Hi,

Even if all libraries in the world are split properly one still needs
a tool to certify that a development didn't load axioms anyway. Do I
miss something?

P.

2016-08-21 23:21 GMT+02:00 Ade Umut Huxtable 
<tkdtezx AT mail.nu>:
> IMHO the standard library is not enough, I think all library developers 
> should recognize that their users might want to stay axiom free, and (if at 
> all possible) give them the choice to do so.
>
> And now I repeat myself: since lib splitting will probably not happen, a 
> tool's usefulnes likely outweights its negative effects.
>
> PS: In my lib for example I hide the axioms making up the IO monad behind a 
> module type, I also demonstrate how a domain can do the same in the 
> abstract-domain branch. Opened an issue about demonstrating how to actually 
> do axiom free development :) https://gitlab.com/mgshrd/beque/issues/18
>
> --- 
> jonikelee AT gmail.com
>  wrote:
>
> From: Jonathan Leivent 
> <jonikelee AT gmail.com>
> To: 
> coq-club AT inria.fr
> Subject: Re: [Coq-Club] Axioms reported by coqchk
> Date: Sun, 21 Aug 2016 11:04:32 -0400
>
> 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
>
>
>
>
>
> _____________________________________________________________
> mail now at http://www.mail.nu




_____________________________________________________________
mail now at http://www.mail.nu