Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: john.harrison@cl.cam.ac.uk
Cc: jgrundy@ra.abo.fi, hol2000@leopard.cs.byu.edu, john.harrison@cl.cam.ac.uk
In-Reply-To: <"swan.cl.cam.:129790:950824164229"@cl.cam.ac.uk> (message from John Harrison on Thu, 24 Aug 1995 18:42:15 +0200)
Subject: Re: Paper available: "HOL Done Right"
Message-Id: <95Aug24.193806met_dst.8087@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 24 Aug 1995 19:38:00 +0200


John wrote:

> But I seem to recall some library standardization effort in the SML
> world. For our purposes, standards for quotations and toplevel
> printers would be the most important thing.

I agree: such general I/O support is vastly more important for the
usability of SML than any new advances in type systems or whatnot that
may seem theoretically urgent. However, cleanly incorporating such
facilities into the type system of ML is itself a research problem (at
least in the case of prettyprinters). Probably the right forum to air
our views is ML2000. However, I imagine that ML implementors and
theoreticians have more sway there than users. It would be foolish to
think that they have our best interests at heart, so I fear that our
current unhappy situation may persist indefinitely. 

Maybe we could draw up a list of concerns from our (the theorem prover)
community and submit it for the ML2000 cabal to chew on. I suspect that
our concerns would mirror the concerns of most users in the general ML
community anyway.

Konrad.