aw1621107 2 days ago

I 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

Reply View 2 replies
  • measurablefunc 2 days ago

    They also use an unverified parser but good to know this exists.

    Reply View 1 reply
    • aw1621107 a day ago

      That'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.

      Reply View 0 replies