Towards a Mechanization of the ECMAScript (JavaScript) Proposal "Temporal"
summary
Mechanization covers about 43 functions of a 500+ function Temporal proposal (≈200 date/time functions), producing 3,000 lines of Rocq code and proofs; one declarative spec required a linear search termination proof that ballooned to ~200 Rocq lines; the RFC grammar for string output is mechanized with a nearly complete RFC 3339 compliance proof; multiple mis-specified preconditions and invalid-value bugs are found and confirmed by Philip Chimento; tooling integration via ES Meta is explored to auto-generate Rocq from spec.
AI-written summary · about
chapters (9)
- 0:00ECMAScript proposals intro
- 1:27TC39 proposal process
- 2:51Temporal proposal overview
- 5:43Mechanizing declarative specs
- 6:47Compliance with RFC 3339
- 8:31Claims for mechanization
- 9:59Mechanization feasibility
- 11:23TC39 workflow integration
- 12:26Q&A
related talks
37mTC39 - From the Proposal to ECMAScript - Step by Step
25mFormal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics(…)
33mESNext: Proposals to look forward to
27mTrusted JavaScript Language Environments with ESMeta
28mTC39 Demystified
43mWhat's up TC39
01h 02mProgramming Language Research for Technical and Social Good: What PL Can Do for Good?
48mWhat's New in JS and the Web