Re: [isabelle] Isabelle Foundation & Certification
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
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
-- 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
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
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
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and