Re: [isabelle] Where to learn about HOL vs FOL?
On Sat, 2 Feb 2013, "Mark" wrote:
Yes, I agree it's very difficult. When I started in theorem proving I
was also struck by the lack of a clear learning path. Isabelle is I
think one of the most difficult to *really* understand how everything
works. You have to understand each of the many layers of Isabelle.
I'm afraid I don't understand these layers, although I would like to at
some stage, but more seem to be getting added as the years go by!
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.
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 difference you see is that we have made conceptual progress in the
last 20 years how to build a high-end LCF-style system. Progess is not
for free, you have to provide some structure, and that inevitaby
introduces some complexity.
In HOL Zero, trustworthiness and understandable implementation are top
of the list (they go hand-in-hand in my opinion), but of course it is
very basic and no good for creating proofs.
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. I would put more trust on OpenTheory
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and