Re: [isabelle] Isabelle Foundation & Certification

Dear Larry, Andrei,

> Your position here puzzles me now as much as it did the last time we talked about this. Let's forget about Isabelle/HOL for a second, and think of a logic L with axioms and deduction rules, but no definitions. 
> Further, assume that L is known, or strongly believed to be consistent, in that it does not prove False. Now consider L_D, the logic L augmented with definitional mechanisms. This augmented logic should of course not prove False either! Writing meaningful definitions is the user's responsibility, but having the definitions consistent is the logic L_D's responsibility. Guaranteed consistency distinguishes definitions from arbitrary new axioms -- I learned this years ago from your papers and books.

I can only second this. After reading books like the Isabelle tutorial, which has Larry as a coauthor, I developed a certain understanding for what "definitional" and "foundational" means, and was for many years under the impression that there was a strong consensus in the proof assistant communities. In this context, I find Larry's comments rather puzzling. In fact, I agree with almost every single sentence he wrote, but

    To my mind, a soundness bug is when a valid expression or proof state is transformed into something wrong.

violates the very notion of "definitional". At some point, we will have to make up our minds as to whether our definitions are definitions or just arbitrary axioms (and whether "typedef"s count as definition).

Mark's comments, which I just read, also neatly summarizes what I thought until recently was a consensus also shared by Larry.


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