Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Date: Wed, 22 Jun 94 12:26:58 EDT
From: reetz <reetz@ira.uka.de>
To: hol2000@leopard.cs.byu.edu
Subject: RE: Academic software
Message-Id: <"i80fs2.ira.080:22.05.94.10.27.08"@ira.uka.de>

Tom ( tfm@dcs.gla.ac.uk) wrotes:

>However,
>many of them entail work which, from an academic *RESEARCH* point of view,
>is not worth doing

I do disagree on that. Well, I can't have a paper on the
conference XY on that, but I do need these tools to do
research. Dealing with HUGE problems, I really run into
problems with the existing hol. Just one example:
expanding definitions of mutually recursive functions
applied on a large term, I ran into 300MB (!) memory
heap size with rewriting the definitions. Programming
my own conversion resulted into no increase of heap
size at all, but programing eats up my time for research.

Another example: doing hardware verification with
non-unit delays, e.g. a concrete 100ns delay of module
X results into 100 SUC's, which isn't fun either.

Yet another example: convincing students to do a programing
job/study with the existing hol is very hard when another
institute right next door says: "hey, forget about learning
sml, hol, proving, and fighting with uncaught hol error for 
half of a year until you are finally ready to do something real. 
Here, you can program using C++ directly, use graphical tools..."

I express these things a little bit provocative, because these
things do have an impact on research. IMHO, some
researchers may need to run larger examples to convince other
people that they can't not only deal with toy examples, but with 
``real'' stuff, too (even it is not sooo ``real'' yet ;-). Here, we
do need a better hol in every point of view.

>It seems therefore crucial to get non-research funding to support these
>activities.

That would be the salomonic solution :-)

Ralf.