Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <13254.9301131405@godel.dcs.ed.ac.uk>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: Bottleneck in HOL (was Re: BETA_CONV)
Date: Wed, 13 Jan 93 14:05:35 GMT
From: Mike Fourman <mikef@uk.ac.ed.dcs>


David Shepherd <des@uk.co.inmos> writes

> The result is
> that the free variable evaluation is performed 100 times where a
> carefully coded, but "dirty", version would only do this once. The
> result is that I have various (simple) design transformations which> take 5 to 10 minutes to do in HOL - I've seen a recent demo of Abstract
> Hardware's Lambda/DIALOG system which does similar  things virtually
> instantaneously.

I'm glad to see that we've achieved something :-) However, I must point
out that LAMBDA achieves this performance, by a carefully coded *AND
CLEAN* proof system. The architecture of the LAMBDA proof assistant is
influenced by ISABELLE as well as other members of the LCF/HOL family.
This fundamental design decision provides the appropriate primitives to
support our style of design synthesis.


> Perhaps with a HOL written in SML (such as ICL HOL or hol90) it is
> possible to use the module structure of SML to flag (and limit) the use
> of such steps outside the core system (i.e. by seeing if a module needs
> to import mk_thm you know whether it may be insecure and thus needs a
> better check). Also, for pedants, you could always provide a clean
> version of the same module.

We also realise that designers are willing to rely on many informal tools,
They will not use formal methods if they cannot be integrated with these
informal tools. The next release of LAMBDA will include a system of 
tagging results that depend on external tools (for example, model
checkers, simulators, or direct user input). This will allow users to
appeal to (supposedly reliable) oracles, but will ensure that any
consequences are appropriately annotated.

Basically, we agree with David's analysis of the problems of moving proof 
techniques into "real world" design. Abstract Hardware Limited is actively
addressing these problems.

Mike Fourman (Director, Abstract Hardware Limited)