Continuing woes in reading the ES6 spec language

Gareth Smith gds at doc.ic.ac.uk
Tue Sep 17 08:53:44 PDT 2013


Andreas Rossberg <rossberg at google.com> writes:
> A spec is a system which (a) wants to be transparent (as opposed to
> encapsulated), and (b) is pretty much closed-world (extension points
> notwithstanding). Consequently, none of the advantages of OO apply,
> and it becomes primarily a barrier.
>
> (I'm not proposing any change to that at this stage, obviously. But it
> is a growing technical debt that we might consider clearing at some
> point.)

If it's helpful, some of us at Imperial and Inria have been working on a
machine-readable (using the Coq theorem prover) operational semantics
for ES5. At the moment we think that the ES5 standard is usually easier
to read for intuition, but we hope that the Coq code will sometime be of
use to readers looking for a certain kind of precision.

The project also comes with a reference interpreter, which we prove
correct according our operational semantics, and test using test262.
There's a good video-intro to the project here:

https://air.mozilla.org/trusted-javascript-spec/

...and I'm always happy to chat.

Thanks,

Gareth

http://jscert.org


More information about the es-discuss mailing list