ML as the ES4 spec meta-language

classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

ML as the ES4 spec meta-language

Brendan Eich-2
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

Reply | Threaded
Open this post in threaded view
|

Re: ML as the ES4 spec meta-language

John Cowan
Brendan Eich scripsit:

> We seem to have chosen ML (OCaml with call/cc, probably) as the meta-
> language for the ES4 spec.  

That's why it's called ML (MetaLanguage); ML began as a metalanguage.
I wish you were using SML instead of OCaml, but I suppose I can learn.

--
A few times, I did some exuberant stomping about,       John Cowan
like a hippo auditioning for Riverdance, though         [hidden email]
I stopped when I thought I heard something at           http://ccil.org/~cowan
the far side of the room falling over in rhythm
with my feet.  -- Joseph Zitt

Reply | Threaded
Open this post in threaded view
|

Re: ML as the ES4 spec meta-language

Brendan Eich-2
On Oct 20, 2006, at 4:14 PM, John Cowan wrote:

> Brendan Eich scripsit:
>
>> We seem to have chosen ML (OCaml with call/cc, probably) as the meta-
>> language for the ES4 spec.
>
> That's why it's called ML (MetaLanguage); ML began as a metalanguage.

Yeah, we know.

> I wish you were using SML instead of OCaml, but I suppose I can learn.

It's not hard :-P.

/be


Reply | Threaded
Open this post in threaded view
|

Re: ML as the ES4 spec meta-language

Brendan Eich-2
On Oct 20, 2006, at 4:19 PM, Brendan Eich wrote:

> On Oct 20, 2006, at 4:14 PM, John Cowan wrote:
>
>> Brendan Eich scripsit:
>>
>>> We seem to have chosen ML (OCaml with call/cc, probably) as the  
>>> meta-
>>> language for the ES4 spec.
>>
>> That's why it's called ML (MetaLanguage); ML began as a metalanguage.
>
> Yeah, we know.
>
>> I wish you were using SML instead of OCaml, but I suppose I can  
>> learn.
>
> It's not hard :-P.


I should add, more constructively, that we are not using the  
Objective part of OCaml; in fact we are trying to use a subset that  
will be easy for SML folks to read and write.  But we need the call/
cc patch to OCaml, because we do not want to model an ES4 stack  
machine or continuation machine.  We want the meta-language to  
support call/cc directly.

This is a pragmatic decision, and there are other ways to skin the  
cat for sure, but they tend to taint the entire reference  
implementation and make it obscure.  We believe we can keep this call/
cc monster in a box, so that it does not taint the spec and break  
abstraction everywhere.  It is needed only for yield and perhaps a  
few other hard cases.

/be

Reply | Threaded
Open this post in threaded view
|

Re: ML as the ES4 spec meta-language

Nicolas Cannasse
In reply to this post by Brendan Eich-2
> 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.

Best,
Nicolas