[Why3-club] permut fix

Jean-Jacques Levy jean-jacques.levy at inria.fr
Wed Mar 12 09:23:27 CET 2014

Dear JC,

Le 12 mars 2014 à 15:55, Jean-Christophe Filliatre <Jean-Christophe.Filliatre at lri.fr> a écrit :

>> ‘axioms of Why3 translated to Coq statements, then proved in Coq’!!
>> It means that these axioms have other def in Coq ?? So you define a
>> model starting from what ? I understand that you prove Lemmas. But
>> axioms ?? 
> ..... 
> But the point is that, as Guillaume explained, there are no more axioms
> in Coq. Thus, if false could be proved in Why3, then it could also be
> proved in Coq, which would prove Coq to be inconsistent.

so it’s assuming that all Why3 axioms are expressible in Coq with relations about total functions, which is surely not the case of any axiom with computable (total) functions, but which must be the case for common ones. 

I never understood how many axioms Coq is relying on. But I can buy that Coq 8.4 release is consistent :-)  


More information about the Why3-club mailing list