SML vs Ocaml for ECMA script spec.
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
> 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.
> 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:
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.)
More information about the Es4-discuss