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



I'd say from the point of view of constructing real proofs this inaccessibility is a real problem. Are there proof statements concerning the formal properties of Isabelle?

Steven



On Feb 4, 2013, at 7:10 AM, Makarius <makarius at sketis.net> wrote:

> 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.
> 
> 
> 	Makarius
> 






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