JSExplain discussed at ECMAScript standards committee meeting
Thomas Wood attended the latest ECMAScript standards committee TC39 meeting this November in San Francisco.
In previous meetings, we have presented a prototype of our JSExplain work to the committee and discussions with committee members at the latest meeting furthered the design directions that JSExplain should take, to assist their needs with drafting revisions to the specification.
JSExplain is a reference interpreter derived from the JSCert project, with a user interface designed to assist someone in their understanding of the workings of the ECMAScript language. It is hoped that in the long run, the language the JSExplain specification is written in will closely match the English language of the specification. Using it as an aid to drafting the specification will be the natural next step, with the added advantage that the new features being proposed can be tested and experimented with interactively during their development.
It is envisaged that the JSExplain specification will be extractable for use in theorem provers to prove theories about the language, for example, the soundness of the invariants specified for Object internal methods.
A preliminary prototype version of JSExplain is available, along with the source code.
JSExplain is a collaboration with Charguéraud and Schmitt of INRIA.
Thomas has also agreed to assist with the Regular Expression Lookbehind Assertions Proposal targeted for the ES2017 specification.