Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Fri, 14 Jul 1995 16:48:49 +0200 (METDST)
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
To: info-hol@leopard.cs.byu.edu
Subject: easy HOL?
In-Reply-To: <199507141222.AA138094551@bobcat.cs.byu.edu>
Message-Id: <Pine.HPP.3.91.950714160751.270Y-100000@muddy.cs.ruu.nl>
Mime-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII

In response to the discussion about 'easy HOL' --if I may call the
topic so--, I have few things I want to add.

Tim Leonard pointed out that it is quite impossible to use HOL
effectively without first learning its vast library of functions (and
facts). He suggested to make some sort of small HOL for people to
learn. I would like to express my full agreement to his idea. 

I guess the point is not to make HOL simple, but to provide an
introductory documentation, in which we guide a newcomer to use basic
mechanics of HOL. We already have a HOL Tutorial book. When I learned
HOL, I used the tutorial. After some weeks I managed to write quite
decent proofs. Nothing sophisticated though.

Obviously, I found the Tutorial adequate. Still, I feel its
presentation can be improved. It is still 100 pages long. For someone
who already knows formal methods I think it is a bit less
to-the-point. For someone who is not familiar with formal methods, 100
pages is perhaps a bit too long to discover how you can discharge an
assumption. I exagerate a bit. But my point is, if I may repeat, I
think the tutorial can be improved, that can mean great difference.

The second point that Tim seemed to imply, is to provide sort of
'simple HOL interface'. That would be nice if it is possible --and I
think that should not be an overly complicated project. 

Whether or not a new user should be first told about automatic tools
or about basic HOL mechanics, I think it's a matter of taste. I can
imagine that some people would rather see some results first. It does
well to motivate your effort. Anyway, I guess Phil Windley has a valid
point. Perhaps we ought to consider integrating more automatic tools
in the future version of HOL.

--Wishnu Prasetya.