Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@ted.cs.uidaho.edu
Subject: HOL portability
Message-Id: <93Jun22.181837met_dst.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Tue, 22 Jun 1993 18:18:26 +0200


Richard Boulton writes:

> 1. HOL88 can be used on (what are now) low performance machines, e.g.
>    Sun3 with 8 Mbytes; HOL90 requires LOTS of memory to perform
>    effectively.

I think Richard is wrong in identifying hol90 as requiring LOTS of
memory; rather it is SML/NJ that requires lots of memory. You have to
consider the implementation of the logic as distinct from the
implementation of the metalanguage.

Larry Paulson writes:

> It is a pity if HOL90 only works with one particular implementation of
> Standard ML, since other implementations (notably Poly/ML) are more
> efficient.

I think Larry is not completely precise when he talks of the efficiency
of PolyML; PolyML is relatively quick at compiling, but is benchmarked
as being 2 to 3 times slower than SML/NJ when running compiled code.

PolyML is a very good implementation of SML and it is suitable for
small-memory machines. hol90 versions 1 and 2 were implemented in PolyML
in fact. When I ported hol90 to SML/NJ, I found that it was hard to go
back to PolyML. One reason was that PolyML's pattern match compiler
couldn't handle the large number of patterns in the code produced by
ML-yacc for the HOL term parser. (I think this has been fixed lately.)
Another reason is that (as far as I know) PolyML only runs on Suns.
Finally, PolyML costs money. So in the short term, it was easier to
implement in SML/NJ. In any case, I do not think that a port to PolyML
would be very difficult. Any volunteers?

Another ML that is good for small memory machines is caml-light. An
implementation of hol90 in this dialect would be very portable as well,
since it's a byte-code interpreter. For instance, it has recently been
ported to the ALPHA, the first ML to have that honor. The caml dialect
also has the "virtue" of being close in syntax to Classic ML. Is anybody
interested in a port to caml-light?

This ML discussion illustrates a weak point in what is traditionally
seen as a strength of HOL implementations: access to the programming
metalanguage. Having access to ML means that the specification of your
theorem proving system becomes much larger, since you have to include
the programming language. If we had a system where one issued only proof
commands, portability would be much simpler.


Richard> 2. HOL90 is not as mature as HOL88, and in my opinion has only
Richard>    recently become mature enough for serious use. 

This is a terribly ambiguous statement. Others have used hol90 seriously
for at least the past 2 years. Certainly the system is not in a mature
state, documentation-wise, since it depends on the hol88 documentation.
In most other respects, I think it is at least as, if not more, mature.
(Current failings in the system: lack of separate compilation for
libraries, sprawling theory files (in some cases), and need for some
sort of overloading facility in the parser.)


Richard> However, HOL90 is still a lot less stable than HOL88.

The stability of hol88 is arguable. In the last week or so, we've had
the following messages:

> From:	Wai Wong <Wai.Wong@cl.cam.ac.uk>
> It has been found that the ML function type_in in HOL88 has some
> undesired strange behaviour. 

>From:	chou@cs.ucla.edu
> HOL88 seems to be unable to parse certain object-level lists:

These bugs, and many more that come up, all occur in moldy,
macro-encrusted Lisp code which, by all accounts, is a pain to maintain.
Why persist?


>4. HOL88 requires a Lisp interpreter/compiler. HOL90 requires Standard ML.
>   I believe that Lisp is much more widely supported than Standard ML (correct
>   me if I'm wrong), so HOL is, in some sense, in safer hands with Lisp.
>   Is Standard ML going to flourish? Or will it die because of Lisp, Haskell
>   or some other language? (I'm not trying to put SML down --- I like it, but
>   can someone `in the know' comment on just how widely used SML is?)
>   Of course, we can look at it the other way and say that Standard ML has a
>   much better chance with the HOL community using and supporting it!
>   We are however in danger of putting all our eggs in the SML of New Jersey
>   basket.

I for one am not losing any sleep over this. In my opinion, the major
virtue of hol90 is that it is written in a single language. What ML it's
in or whether it's in ML at all is kind of irrelevant (provided the
metalanguage can provide security in the production of theorems).

If you want to talk about programming, SML is a better language than
Classic ML for writing large programs in. It has a module system, good
compilers, and is the subject of much active research. (to Larry) Yes,
there is a Definition, but the Definition is silent about important
things like object-language embedding facilities and pervasive
libraries. The Definition was written at a certain state of knowledge
about ML; research has advanced that knowledge, and to not take
advantage seems mulish. I wish I knew how to make this jibe with
portability concerns, though.

On the down side, current ML compilers (caml-light aside) certainly need
to be more portable. I think that this is just a matter of time.

Enough already,
Konrad.