ML as the ES4 spec meta-language

Nicolas Cannasse ncannasse at
Tue Oct 24 00:14:24 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! ;-).
> /be

Sounds like a good choice ;)

Keeping the code pure Caml (without the Object system) is also a good
thing, since although OCaml object system is incredibily powerful, it's
also quite difficult to master.

Hope to see some code available soon for review.


More information about the Es4-discuss mailing list