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 right now.

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.


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