The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

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