SML vs Ocaml for ECMA script spec.

Dave Herman dherman at ccs.neu.edu
Wed Oct 25 04:36:44 PDT 2006


> I was suggesting that those who were interested in different 
> specification techniques do it on their own time, and leave you guys 
> alone. :) When the next rev comes out people can flog it out or perhaps 
> have a process to include more detailed specs as clarifying 
> informational addenda...  If I remember correctly RS5Rn is in that 
> style. The prose is the "official" standard and the semantics was 
> "informational".

I see.

> It might be good to have such parallel efforts, as it might help to 
> debug the spec you guys are developing. It's my experience that you can 
> never believe anything is done right, unless you do it two times in 
> different ways.

Sure.

> In particular proving type-safety is best done with a small-steps 
> semantics. However, I don't think you guys want to tackle that in the 

Indeed-- however, it's hard to prove your type system sound if it isn't. 
;) According to the current draft spec, ES4 has a dynamic type system 
with a "verification phase" that may reject some programs. However, 
there is no Milner-style guarantee if the static checker blesses your 
program; any expression may still generate a runtime type error.

Basic language safety (in the sense of Appel's "sermon on safety" in the 
Tiger book) is ensured via dynamic types. With a spec in ML, this 
amounts roughly to proving that every case analysis is exhaustive 
(conveniently proved by the ML compiler!), and perhaps strengthened by a 
hand proof showing that certain "can't-happen" cases never happen. Type 
soundness, though, doesn't hold.

(For the very latest on what type soundness means in a language with 
mixed static and dynamic types, I recommend Sam Tobin-Hochstadt and 
Matthias Felleisen's upcoming paper at DLS:

     http://www.ccs.neu.edu/home/samth/

The basic refinement of Milner's statement is something along the lines 
of "programs with well-typed modules only go wrong due to untyped 
modules." However, we don't quite have such a system.)

Dave



More information about the Es4-discuss mailing list