Re: [isabelle] Isabelle Foundation & Certification

On Sun, 20 Sep 2015, "Mark Adams" wrote:

Wouldn't it be highly relevant to include HOL Zero in the systems you
consider in your list?

Here is the missing entry:

** HOL Zero **

Minimalistic re-implementation of HOL, designed with trustworthiness as its top priority.

  [small]      +++
  [ML]         ++
  [thm]        +++
  [defs]       +++
  [context]    0
  [logic]      ++
  [formalized] 0

[ML] Unlike HOL-Light there are explicit provisions to avoid unsafe aspects of OCaml. Architectural weaknesses remain, since user ML scripts operate directly on the OCaml toplevel.

[small], [thm], [defs], [context], [logic] similar to HOL Light.

I.e. it is mostly like HOL Light, but [ML] gets ++ (like HOL4 with its SML basis), because extra care is taken to avoid weaknesses of OCaml.

A fully managed ML environment as in Isabelle would get +++.


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