I’m interested in MLton because of the chance that it might be a good vehicle for future implementations of the HOL theorem-proving system. It’s beginning to look as if one route forward will be to embed an SML interpreter into a MLton-compiled executable. I don’t know if an extensible interpreter of the kind we’re looking for already exists.