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

Konrad Slind writes:

>OK, I will. As long as one is in a situation needing garbage collection,
>one may as well stick with a language that already has a garbage
>collector. "Efficient C implementations" in such cases usually turn out
>to be slower and buggier.

I disagree. There is no need in using a waisting copying garbage collector for
C programs as in ML. You ``just'' need to choose the right data structures
and handle your allocation/deallocation carefully. IMHO this is just an
exercise on how good you are in data structures & algorithms! Good
programmers can always do be better in choosing specialized data
structures than the more general approach of garbage collectors.
I also disagree that C programs are slower. Take a look at the archive
on comp.lang.ml. Several people have posted benchmarks there and C programs
were always faster with a factor 1.3 - 3. Even if they are slower, I don't
care that lot because as long as my machine is swapping all the time because
of high memory consumption, ``slower'' and less memory is much faster
because everything fits into the main memory of the machine.

I agree that C programs are more difficult to write than ML programs and thus
the probability of a bug may be larger in C than in ML. But again, writing
good C programs is possible, running a program needing several hundreds
of MB memory is not feasible, maybe even not possible.

O.K. Discussions on C versus ML can go on forever. I just wanted to note here
that ML is IMHO not the one, perfect solution and that other parents have
nice children, also. HOL depends too much on a not-so-frequently-used
programming language, which often makes portability a problem. What if, e.g.
SML/NJ is suddenly dying and no other FULL implementation of SML is in
sight?? C was there, is there and will be there in a variaty of
implementations. In order to put HOL into the real world,
HOL2000 should be programmed in a more usual programming language with
less memory consumption.