4 ms·
How about a formally verified runtime that takes the JS spec & constructs a runtime by converting the spec w/ incremental & verifiable transformations into an e
by measurablefunc 1y ago
How about a formally verified runtime that takes the JS spec & constructs a runtime by converting the spec w/ incremental & verifiable transformations into an executable runtime?
- aw1621107 1y agoI think you'd need a "proper" formal spec (e.g., JSCert's version of ECMAScript 5 in Coq/Rocq [0]) for that to be feasible. Not exactly sure how "verifiable" would work otherwise. [0]: https://github.com/jscert/jscert https://github.com/jscert/jscert
- measurablefunc 1y agoThey also use an unverified parser but good to know this exists.
- aw1621107 1y agoThat's true, though I think the general point stands - you need a "proper" formal spec to even begin thinking about a formally verified runtime. Presumably if you have a full formal spec a verified parser should be within reach.