Email Gateway (Feb 03 2026 at 20:09): Email Gateway (Feb 03 2026 at 20:09):From: Jan Bessai <jan.bessai@tu-dortmund.de>
Dear Isabelle Mailing List,
some colleagues and I are organizing a workshop on Unsoundness at ECOOP'26:
https://2026.ecoop.org/series/unsound
We would be very happy to accommodate a talk (or two) about Isabelle. In
particular, it would be great to hear how the different parts of
Isabelle (e.g. Isabelle/Pure) have different guarantees, how they
interact and what guarantees you (don't) get from that interaction.
Also, any talk on issues you actually had in any of the Isabelle
sublanguages would be appreciated. Did any of those ever had something
retracted from the AFP?
Feel free to contact me for details if you are interested!
Bests,
Jan
Email Gateway (Feb 04 2026 at 11:35):From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks for your suggestion. Indeed a distinction can be made between Isabelle/Pure and Isabelle/HOL, in view of the enormous amount of specialised tools provided in the latter, and specifically, past issues involving type classes. (Such vulnerabilities are impossible for Isabelle/ZF, for example.)
As far as I know, no soundness bug has necessitated the retraction of a published development using any proof assistant, although 30 years ago some PVS users were complaining that its soundness issues were significant enough to interfere with their work.
I have even written a blog post on such issues recently:
https://lawrencecpaulson.github.io/2026/01/15/Broken_proofs.html
Larry
On 3 Feb 2026, at 20:09, Jan Bessai <jan.bessai@tu-dortmund.de> wrote:
We would be very happy to accommodate a talk (or two) about Isabelle. In
particular, it would be great to hear how the different parts of
Isabelle (e.g. Isabelle/Pure) have different guarantees, how they
interact and what guarantees you (don't) get from that interaction.Also, any talk on issues you actually had in any of the Isabelle
sublanguages would be appreciated. Did any of those ever had something
retracted from the AFP?
Email Gateway (Feb 12 2026 at 19:28):From: Makarius <makarius@sketis.net>
On 03/02/2026 21:09, Jan Bessai wrote:
Did any of those ever had something retracted from the AFP?
Short answer: no.
Makarius
Last updated: Feb 22 2026 at 05:16 UTC