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

> 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.


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