Re: [isabelle] Where to learn about HOL vs FOL?


That was quite an aggressive email.  I feel I have to respond to your points
in order to defend my work.

on 4/2/13 3:10 PM, Makarius <makarius at> wrote:
> I don't know anybody who really understands everything of Isabelle.  But I
> do understand its construction principles, and have a vague idea of the
> vast space of possibilities resulting from it.  This is just plain-old
> modularity taken seriously.
> There is no need for users to understand everything.  I use Linux everyday
> without having a clue how it is done these days, although I know about
> certain general principles as a mental model.

Yeah, but I'm talking here about people who, for whatever reason of their
own choosing, want to really understand how Isabelle works.  I'm not talking
about "ordinary users".

>> But the main priorities for the implementors of Isabelle, as I
>> understand it, have been usability and power, and having an
>> understandable implementation comes way down the list.
> Understandable implementation is actually the main priority in Isabelle.
> Otherwise this vast system could not be managed at all.

The main priority?  I don't believe that!  You've already said that you
don't understand everything.  The extra layers that have been introduced
massively complicate the implementation, but are done with the good
intention of improving usability (and maybe other reasons as well).  So, if
understandable implementation were the *main* priority then why on Earth
would this have been done?

> This discussion has bounced between the HOL and Isabelle mailing lists
> several times already.  HOL Zero is as tiny that you see the problems
> inherited from OCaml immediately.

As far as I understand, the only trustworthiness issue that you have with
HOL Zero is that it is implemented in OCaml.  Firstly, HOL Zero addresses
the main OCaml vulnerabilities to do with string and integer representation,
and in any case can be relatively easily ported to SML, and I even intend to
do this at some stage, as you well know, so please stop banging on about
this.  Secondly, the implementation language is secondary here.  The primary
problem is designing and implementing a system that itself has no intrinsic
trustworthiness-related flaws.  All other HOL systems other than HOL Zero
have not managed to do this because they have flaws in their pretty
printer/concrete syntax design.  Their implementors either admit these flaws
or brush them under the carpet with "well normal users are not malicious so
would never in practice exploit these".  Only HOL Zero has no such known
flaws, and it even has a bounty of $100 for anyone who can find one.  So,
please, try to say something positive about HOL Zero's trustworthiness.

> I would put more trust on OpenTheory right now.

It is a misconception that HOL Zero is competing with or incompatible with
Open Theory.  HOL Zero is a HOL system.  OpenTheory is a system for porting
theory and proofs between HOL systems (and perhaps other systems).  Someone
could write an Open Theory importer or exporter for HOL Zero just as much as
for any other HOL system.  If they did, this would boost the credibility of

> But we don't have users in the queue to ask substantially more
> trustworthyness than is there in Isabelle already.  Most users actually
> want less, but I have no inclination to reduce the general robustness of
> Isabelle either.

Yes, there is no such queue of users.  Isabelle quite rightly concentrates
on usability.  This does not mean that I am wrong.


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