Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu
In-Reply-To: <"irafs2.ira.986:17.03.95.12.17.32"@ira.uka.de> (message from reetz on Fri, 17 Mar 1995 13:17:15 +0100)
Subject: Re: memory consumption of load_theory in HOL90.7
Message-Id: <95Mar17.171508met.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Fri, 17 Mar 1995 17:15:04 +0100


With respect to the merits of chucking SML and just getting on with it,
Ralph makes a few good points. SML programs *do* often run slower than
their C equivalents, sometimes because the C versions are taking
advantage of non-portabilisms, like the hack noted in John Harrisons's C
implementation of BDDs (something about using word alignment conventions
to efficiently encode complement edges, I think). However, there are
more essential reasons, for example a paper analyzing typical SML
executions has observed that SML/NJ programs allocate an order of
magnitude more memory (than other SML implementations, presumably), thus
making an efficient garbage collector correspondingly more
important. Finally, I think SML is a difficult language to write a
compiler for, and so there are problems with portability and questions
of whether one ought to use the full language when writing an
application.

On the other hand, one should be careful not to confuse problems with
hol90 or SML/NJ to problems with the SML programming language. [Just
remember, it's always a mistake to generalize. :) ] Portable and
memory-efficient versions of SML already exist, and I expect more to
become available. More important, ML's type system and associated
inference algorithm represents a fundamental advance in programming
languages. I would not willingly abandon this for the pleasures of
casting to char *.

Finally, if Ralph does want to rewrite HOL in C, he may find a recent
comp.lang.ml note by someone at CMU (Gene Rollins, I think) to be
interesting, wherein they state that the forthcoming SML/NJ release
makes a very pleasant environment to write C programs in!

Konrad.