Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu



A number of bugs in PVS had this effect too. As with your example, even the most careful user could not escape. And thatâs precisely my point: soundness bugs often have consequences. 

Larry Paulson


> On 21 Aug 2016, at 21:02, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
> 
> 
>> As far as I know, this was the case for any problems (either implementation bugs or more substantial problems) that were found in other provers.
> 
> I believe the soundness bug found in the Coq termination checker in December 2013 was hard to fix without breaking libraries -- I'm not sure what the exact resolution was and how much of an impact it had, but I believe it took them over one year to sort this out precisely because of the tension between soundness, expressiveness, and compatibility. Perhaps somebody with more knowledge about this should comment, but regardless it's dangerous to draw the conclusion that all soundness bugs can be fixed with no impact on real, legitimate applications.
> 
> Jasmin
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.