Everything else is secondary. It is nice that Andrei's and Ondrej's paper establishes certain logical properties of their improved system, and it is interesting to discuss these properties, but the most important thing is the actual addition of a cycle check to the code.
Tobias On 18/09/2015 17:28, Makarius wrote:
Back to this thread after the initial round of discussion ... First of all, I don't see much of a technical problem here, but mainly a social one. A bit too many things not explicitly spelled out; a bit too many rumors and private mailing threads about "Isabelle/HOL is inconsistent", already since summer 2014. For years we have tried to establish isabelle-dev (also isabelle-users) as a professional channel for open discussion about presumed problems, potential solutions, proposals for changes etc. That works out half way, and needs more efforts. On other mailing lists (e.g. Coq-club) I see routinely the discussion of genuine logical breakdowns without much excitement about it. The Coq/HoTT implementation even seems to require patching Coq to disable critical checks, for the elite of users who really know what there are doing at the bleeding edge ... The present thread is essentially about the paper "A Consistent Foundation for Isabelle/HOL" by O. Kuncar and A. Popescu, ITP 2015. On 26-Mar-2015, the authors had sent me a draft for comments, also pointing out that it was submitted to ITP and referring to the patch http://www21.in.tum.de/~kuncar/documents/patch.html On 07-May-2015, rather late, I answered that mail as follows: I am now back to this in the second round. It is still on the pile of things labeled "very long and not immediately clear". For now I can only say it is not relevant for the Isabelle2015 release, unless you say there is a new deviation from known and documented "Typedef axiomatization" in the isar-ref manual. To which I got an answer agreeing with the "unless" part, i.e. no need for immediate action. Thus it went back on the top of the pile of things that need attention soon. Remark: The above-mentioned "Typedef axiomatization" is section 11.5 in http://isabelle.in.tum.de/website-Isabelle2015/dist/Isabelle2015/doc/isar-ref.pdf -- a section of that title first appeared 2010-03-13 in changeset 93603d7b8ee9. Before that there was an oral tradition of "axiomatic type-classes are definitional, and HOL typedefs are axiomatic". Before we proceed, we also need to recall the professional routine of the Isabelle release process, which was established for Isabelle2008 after years of chaos. In particular: * Substantial feature additions happen only *after* a release. * Changes just *before* a release need to address important backdrops from already established or expected behaviour. * If in doubt, it is better not to apply any "hot fixes" at all. * Complaints about already released versions are ill-typed. This particular change is a genuine feature addition, not a fix of anything broken. So it did not get into Isabelle2015 -- and there is no need to consider Isabelle2015-1. To understand this, I now refer to the published paper, as it is available from http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-itp2015.pdf I refer only to the general exposition in sections 1, 2, 6. I still need to study the technical parts, and more importantly the full version of the technical report http://www.eis.mdx.ac.uk/staffpages/andreipopescu/pdf/IsabelleHOL.pdf -- link broken!? The introduction of the paper talks a lot about "consistency" in a way that I usually try to avoid, because it tends to be a rather weakly defined, and different people think of slightly different things. "Inconsistency" is certainly very bad, but what does it really mean? And what is gained by "consistency"? For genuine definitions, I would expect much more than that. Part of the confusion is also caused by treating the system called "Isabelle/HOL" in the paper like another implementation of the Cambridge-style HOL systems, e.g. HOL4 or HOL-Light. I had serious problems to recognize the system where I am involved for 2 decades from that text. In reality, Isabelle/HOL is a library or "application" within the Isabelle framework (Isabelle/Pure). This has a variety of consequences for many aspects, including the foundations. In particular, there is not "the kernel" that establishes certain formal virtues. The core of Isabelle/Pure is built up in various stages -- both the concepts and the implementation, and the Isabelle/HOL application augments that later. This adds considerably complexity in understanding the construction of the whole edifice. But our overall architecture also provides structural integrity and scalability, and thus allows the huge applications we see today. Projecting the combined Isabelle/Pure + Isabelle/HOL tower down to the logical core, we are left with two different concepts: (1) The inference system, to establish proven "thm" values. (2) The management of formal theory content, with some notion of "definitional theory extension" among other things. Both are mixed up in the paper! This can be explained from the classic Cambridge HOL standpoint, where there is a rule of the inference kernel to make a constant definition or type definition. We don't have that in Isabelle, although I have re-adjusted some ML programming interfaces in recent years, to approximate that view a little bit. This means in Isabelle, only (1) works vaguely like the inference kernel of HOL, and many more things would have to be explained about just that if the discussion would go to the full depth. In contrast, Isabelle theory content in the sense of (2) used to be mostly unchecked over many years -- Larry still speaks from that perspective until today. Within a logical framework, the user just claims "rules" axiomatically and then does a little bit of inferencing. He normally knows what he is doing, or at least thinks so. There are no big applications and libraries from other people. Since this is surely impractical for big application, we have retrofitted more and more integrity checks to the operations that add theory content, without closing up the process formally so far. Thus the Isabelle2007 version of 'defs' together with some recent improvements by Ondrey Kuncar according to http://www21.in.tum.de/~kuncar/documents/kuncar-cpp2015.pdf could be taken as a robust check concerning constant definitions in Isabelle/Pure (which are re-used as constant definitions in Isabelle/HOL). HOL typedefs were never part of that, and that was known to the people working in that spot. It is also made explicit in the isar-ref manual, as cited above concerning "Typedef axiomatization". The paper says on page 2 just before Example 2 "Unfortunately, the improper management of the intermixture leads to inconsistency". There is no "improper management", there is no management of constdefs vs. typedefs at all. And that is documented explicitly for several years. (The paper fails to quote that documentation.) This aspect of Isabelle can be certainly improved, and this is what the paper is actually about. So it does not "fix a big" in Isabelle, it adds more features, namely more structural integrity of the Isabelle/HOL library, within the existing Isabelle/Pure framework. This proper distinction also explains, why typedefs were not treated in the past, because it is hard to understand them in generic Isabelle/Pure, without an unfriendly takeover of the framework by HOL troups. A few more notes on the paper: I actually liked the "Inconsistency Club" versus "Consistency Club", although it is hard to define that boundary. Just a single Boolean value to measure the reliability and robustness of a proof assistant in black or white is a bit lacking. Apart from shades of grey, such a measure desparately needs more than one dimension. Within the given all-or-nothing model, I am tempted to claim the "Consistency Club" to be empty. Why is HOL-Light in there? It has a proven model (without treating definitional mechanisms), but its implementation greatly suffers from unsafe OCaml. (The Coq guys need to add a lot of unproven code complexity to circumvent OCaml weaknesses in their system.) To me the great work on end-to-end formalization of CakeML and HOL kernel  and the other work on Milawa  looks like the real candidates for Consistency Club membership. I am looking forward to see real-world proof assistants in that category in the future. When the ITP community has reached these lofty hights of approximative soundness, we will probably see attacks like the now infamous Row Hammer https://en.wikipedia.org/wiki/Row_hammer -- or worse. This should not discourage such great projects of fully-verified proof checkers. In particular, we should find ways to export Isabelle theory content and proofs to such next-generation tools. I personally don't think that one big system can do everything at the same time: being ultra-reliable, scalable, all-powerful. As a concrete medium-scale project, one could put the existing partial connection of Isabelle/HOL to OpenTheory http://www.gilith.com/research/opentheory into a usable form, especially a bidirectional one. Makarius
Description: S/MIME Cryptographic Signature