ML as the ES4 spec meta-language
brendan at mozilla.org
Fri Oct 20 12:36:13 PDT 2006
We seem to have chosen ML (OCaml with call/cc, probably) as the meta-
language for the ES4 spec. This is hot of the presses, but it looks
like the right choice, and any change that moves away from it will
take unlikely effort and a better candidate language. We were faced
with the arduous task of inventing our own sound meta-language, and
it started looking like ML with customizations.
This means we will have a reference implementation, with all the
software engineering overhead that implies. But it will be an
implementation whose goal is clarity and soundness, not space or time
performance. And with some work, as Cormac Flanagan points out, the
reference code (or probably a subset of it) could be used with Coq to
do automated proofs.
We will make the reference implementation available in due course, as
open source. We will welcome contributors (Hi, Nicolas! ;-).
More information about the Es4-discuss