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:

  www.proof-technologies.com/flyspeck/qed_paper.pdf

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.


	Makarius





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