The Coq mailing list

["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