Re: [isabelle] Isabelle Foundation & Certification
On Sun, 20 Sep 2015, "Mark Adams" wrote:
I should mention that a lot of the issues and ideas mentioned in this thread
are discussed in my recent paper:
Interesting paper. Here are some notes, after skimming through it.
- The term "LCF approach" is used in the tradition of HOL88 to include
definitional principles, but LCF (and Isabelle) did not have that from
the outset. For papers that talk about trustworthyness of provers, the
distinction of [thm] vs. [theory] -- according to my earlier
categorization -- to avoid great confusion.
- Concerning ML (SML or OCaml) as "system implementation language" and
weaknesses coming from exposing that to the user: LCF did not have this
problem, the LISP core was clearly separated from ML. The HOL family
after HOL88 collapsed everything to one ML toplevel. Isabelle is closer
to original LCF by running user-code in a managed Isabelle/ML
environment that is not the same as the underlying SML.
- Isabelle does not have "proof scripts". The proper terminology is "proof
texts" or "proof documents". The point is that there is more structural
integrity enforced by the system, on some controlled language that is
not just the implementation language of the prover.
- "Allow uncontrolled adaption to the way formulae are displayed": cf.
check/uncheck phases in Isabelle, which admit arbitrary non-sense on
input and output of terms, without any formal barriers. These are
official programming interfaces, not back-doors.
- 3.2.1 interesting notes about HOL Light, including a special
(non-)treatment of typedefs as implicit pre-requisites to proven
theorems. Such a formal record of dependencies (or "proof digest" in
Isabelle terminology) was excluded from the discussion so far. The
question is how "holes" in the reasoning are tracked (non-definitional
axioms, oracles). I think that HOL4 is doing this most thoroughly.
Isabelle only half-thoroughly.
I liked the general approach to port formalizations to other systems for
independent checking. I think the main weakness of the bigger systems
(Coq, Isabelle) is that they have grown into large islands of their own,
islands that could be mistaken as continents. It would be exceedingly
nice to see full OpenTheory connectivity for Isabelle/HOL, although the
addition of overloaded type constructors to the standard portfolio has
moved us one more step away from it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and