ML as the ES4 spec meta-language

Brendan Eich brendan at
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 mailing list