[MLton] HOL's Moscow ML implementation, and pushing MLton to emulate it

[Michael Norrish]

Michael Norrish writes:
> Matthew Fluet writes:
  
> > Scott has the right idea, but one can make it more formal (and more
> > extensible) by using the ideas of embedded interpreters.  See, for
> > instance,
  
> > http://www.eecs.harvard.edu/~nr/pubs/embed-abstract.html
 
> > and
 
> > http://research.microsoft.com/~nick/benton03.pdf
> 
> I've looked at both of these papers, and am tempted to say that we
> need the ideas in them because they're obviously way cool.  However, I
> suspect that we don't need to implement a programming, or "scripting"
> language at all.  Indeed, expressing proofs as programs is arguably a
> mistake, and we should be providing a proof language that is not
> programmable at all.
 
I take this claim back.  I think an embedded ML-Light interpreter
would be just great for us, mainly because it would enable us to keep
using our existing proof scripts which are all "stereotyped SML".
Once this was working, we could think about supporting a new proof
language too.  Such a language would not necessarily be a programming
language, but would be interpreted in just the same way as the ML.

It's also possible that people will find proofs that absolutely
require a bit of custom-programmability.  I don't really expect it,
but it's possible.

So, this leads to the obvious question: has anyone written an
embedded, extensible interpreter for SML in SML already?  (If not, why
not? :-)

Michael.