Sukyoung Ryu (professor at KAIST, Daejeon, Republic of Korea) and Jihyeok Park (assistant professor at Korea University, Seoul, Republic of Korea) have written a report “JavaScript Language Design and Implementation in Tandem” on the results of a multi-year collaboration. JavaScript is the first programming language for which each change to its prose language specification is both “type checked” and “tested” to identify bugs and inconsistencies. This report is downloadable in various formats at https://dl.acm.org/doi/10.1145/3624723.
In this article, Sukyoung Ryu and Jihyeok Park present how to automatically extract a mechanized specification from a prose specification and how useful it can be in practice. Using the example of JavaScript, they show how mechanized specifications can be used to detect conformance bugs between language specifications and existing JavaScript engines in major Web browsers, and to generate more special-purpose JavaScript implementations, such as static analyzers, in a correct-by-construction manner. They propose a new approach to programming language development as a promising direction for the future: first design the language in a mechanized specification and then generate both human-friendly specifications written in diverse natural languages and correct-by-construction implementations and tools from the mechanized specification.
For more information: please contact Samina Husain, Secretary General of Ecma International at media@ecma-international.org.