Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 7 Jun 1994 14:18:43 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA28939;
          Tue, 7 Jun 1994 07:08:50 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA28928;
          Tue, 7 Jun 1994 07:07:48 -0600
Received: from infix.cs.ruu.nl by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA00478;
          Tue, 7 Jun 1994 06:06:41 -0700
Received: by relay.cs.ruu.nl id AA18994 (5.67a/IDA-1.5 
          for info-hol@ted.cs.uidaho.edu); Tue, 7 Jun 1994 15:06:34 +0200
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
Message-Id: <199406071306.AA18994@relay.cs.ruu.nl>
Subject: Why HOL is so large?
To: info-hol@cs.uidaho.edu (hol mailing list)
Date: Tue, 7 Jun 1994 15:06:33 +0200 (METDST)
X-Mailer: ELM [version 2.4 PL23]
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 629

Hi,

I see two applications of HOL. As a theorem prover, mainly in a
hardware design. And as a proof management system, mainly to assist
scientists in writting correct proofs. Unfortunately we are still long
from the day where when every one in the department can engineer his
proof as he would his document with LaTeX now. One of the challange is
the computing power requirement of HOL. Perhaps some one can kindly
explain to me why, for example, HOL requires so much memory to run? Is
this 4-9MB really the bottom line? Of course we can also hope that
memory will become considerably cheaper in the future.

Thanks,

-Wishnu--