Re: [isabelle] Isabelle Foundation & Certification



The length of this dicussion puzzles me. Typedef can introduce inconsistencies, nobody wants this behaviour and nobody needs this behaviour. There is a perfectly clear way to rule out this whole class of unwanted behaviours: do not allow certain cycles. This solution, including code, has been on the table for a year now. By now not just mere users but also certification agencies are worried. This is a pressing issue and it is not rocket science.

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 [20]
and the other work on Milawa [25] 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



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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