Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Date: Thu, 23 Jun 1994 09:07:17 +0930
From: Jim Grundy <jug@itd.dsto.gov.au>
Message-Id: <9406222337.AA14421@itd0.dsto.gov.au>
To: reetz@ira.uka.de
Subject: RE: Academic software
In-Reply-To: Mail from 'hol2000-request@lal.cs.byu.edu' dated: Wed, 22 Jun 94 12:26:58 EDT
Cc: hol2000@leopard.cs.byu.edu

>Ralph writes
>>Tom Writes:
>>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.

I think what Tom was saying here is essentially what you were saying in your
last sentence. For some of us (i.e. people like Tom), _writing_ the tools, not
using the tools is the research.  For such people, the research stops once the
concepts have been demonstrated. For them there is no futher research return
to be gained by spending longer on the problem and making the implementation
neally nice.

So in short, while it would obviously help your research to have a more stable
and better developed tool, whats in it for the guys writing the tool?

Perhaps I could try to answer that myself, I guess if one were to take that
attitude then we should not even be contemplating HOL2000, it is not planned
as a radical departure from the current HOL, so what is in it from a research
point of view?  I think the motivation behind it (and part of the reason for 
the success of HOL) is that many of the people who write HOL also use it.
That is, HOL grows because a group of its users (mostly the ones who
are in Cambridge at the time) go in and enhance the tool whenever they find
that it is not up to the task they are working on.

I think one thing we could do to make HOL2000 a sucess would be to grear up
for some kind of distributed devopment method in which it would be easier for
members of the geographically diverse HOL comunity to propose and implement
enhancements to the tool.  Obviously we would have to avoid a 'too many cooks'
type situation.  So, I would propose - inline with Ralph's earlier comments -
that a house coding style and philosophy be promulgated, and in addition that
all proposed modifications are centrally reviewed.  Proposed changes could be:
incorporated, rejected, or sent back for rewriting.

Well its an idea anyway.

Jim