JavaScript Language Design and Implementation in Tandem

Programming languages have been specified using a wide variety of approaches. Most programming language (PL) specifications are written in unstructured prose, but some are written rigorously to help developers build correct language implementations. For example, Standard ML (SML) was first designed with a formal specification that defined the language syntax and semantics in mathematical notation, followed by a reference implementation of the specification. JavaScript is well known for its language specification, which is written in highly structured prose at the level of pseudocode algorithms. Finally, the specification of WebAssembly provides the syntax and semantics of the language in both highly structured prose and mathematical notation.

Unfortunately, rigorous language specifications do not prevent bugs in language implementations. SML maintains a list of reported bugs, and different implementations have different sets of bugs. JavaScript has many implementation bugs in the JavaScript engines of various Web browsers.

More importantly, it is difficult to get a rigorous language specification right. Despite its complete formal semantics, the WebAssembly 1.0 specification had bugs detected by mechanized proofs of Conrad Watt.³⁵ The developers of the Verse programming language² described the language semantics in rewriting rules and opened a call for participation to the PL community for confluence proofs.

In this article, we 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, we 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. We 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.

We propose a new approach to programming language development: design the language in a mechanized specification, then generate both human-friendly specifications written in diverse natural languages and correct-by-construction implementations and tools from the mechanized specification.

History of JavaScript

JavaScript is the most actively used programming language on GitHub.¹⁷ All Web browsers include a JavaScript engine. It was initially designed and implemented by Brendan Eich in May 1995 as a simple dynamic language that allowed code snippets to be interpreted by Web browsers. In early 1996, companies including Netscape and Microsoft were frequently releasing browser technology, but language standardization was slow and often contentious. To ensure interoperability between different browsers, TC39, the Ecma Technical Committee responsible for standardizing JavaScript, held meetings to create the JavaScript language specification.

Unlike programming languages that “grow up” via a single implementation, JavaScript began with multiple implementations, which guided its specification:³⁶

Richard Gabriel, who attended some of the working group meetings, recalled in a personal communication a not uncommon interaction during these meetings. Guy Steele would ask a question about some edge-case feature behavior. Sometimes Brendan Eich would say “I don’t know,” and sometimes Eich and Shon Katzenberger would be unsure or disagree; in such cases, they would each turn to their respective implementation and try a test case. If they got the same answer, that became the specified behavior. If there were a difference, they would discuss the issue until they reached an agreement.

The history of JavaScript is described in great detail in Wirfs-Brock and Eich.³⁶ The first edition of its language specification ECMA-262, abbreviated ES1, was released in 1997, edited by Guy L. Steele, Jr, in 95 pages. JavaScript developers continued to demand more advanced language features, so ES2 and ES3 were released in 1998 and 1999, respectively. However, attempts to define a fourth edition were eventually abandoned due to the radical changes in a single update that included a variety of new language features, and ES5 was finally released in 2009. Starting with the sixth edition, TC39 adopted the practice of using the year of publication as an abbreviation. Thus, both “ES6” and “ES2015” are informal abbreviations for “ECMA-262, 6th edition.” TC39 also decided to release ECMA-262 annually, starting with ES2015, to ensure rapid adoption of new language features. The latest ECMA-262¹⁰ is a much larger specification at 827 pages.

Now, ECMA-262 is maintained as an open source project¹¹ and follows the TC39 process¹⁴ for handling proposals for new language features. JavaScript contributors propose new features along with specification changes and tests, which are maintained in a separate repository⁶ over six stages. Since 2015, TC39 has successfully published an updated edition of the ECMAScript specification every June, following the TC39 process.

As with the language specification, various companies, including Microsoft and Google, have released their own open source test suites for JavaScript. In 2010, TC39 decided to maintain Test262,¹⁵ an open source JavaScript implementation conformance test suite. After working through many policy and licensing issues, Test262 is now an integral part of TC39’s development process. Every new ECMAScript feature must be accompanied by its tests before it is incorporated into the ECMAScript standard. At the time of writing, Test262 consists of 48,854 tests.

Correctness and Conformance of the Specification and Implementations

Along with its reputation as the most widely used language, JavaScript is also well-known for its unintuitive semantics due to its highly dynamic nature and extensive use of implicit type conversion. As a result, there are many sophisticated JavaScript examples. Consider the following JavaScript code:

function f(x) { return x == !x; }

Even for this simple function, it is not easy to understand exactly what its behavior is: the function f simply compares the given argument x with its negation, so it looks like it returns false. However, when an empty array is given as an argument, it returns true due to a number of implicit conversions for the negation and equality operators. More specifically, when f([]) evaluates [] == ![], the negation of the empty array ![] evaluates to false because any object represents true. The operands [] and false of the equality operator are then both converted to values of the same type according to the implicit conversion rules defined in ECMA-262. In this example, they both get converted into the same Number type value, 0, so the final result becomes true.

Such counterintuitive semantics often leads to various bugs and security vulnerabilities in implementations. Experienced JavaScript developers often introduce bugs that are difficult to catch due to the extremely dynamic nature of JavaScript. Mainstream JavaScript engines, such as V8, JavaScriptCore, SpiderMonkey, and Chakra had various bugs that were more harmful than bugs in JavaScript programs.³⁴ They also had security vulnerabilities that could lead to remote attacks. For example, a high-severity bug in V8, tracked as CVE-2021-21224, was widely exploited in April 2021.³³ Besides, it is more challenging to correctly develop special-purpose JavaScript implementations that require a deeper understanding of the specification for specialized language semantics. For example, most existing JavaScript static analyzers^19,20,23 require a sound abstraction of the language semantics to guarantee the soundness of their analysis. However, because they need to consider not only concrete semantics but also how to abstract them soundly, they have been plagued by soundness bugs²⁵ for unusual edge cases in language semantics.

ECMA-262 also had a number of bugs. Consider the following Math.round built-in library function (specified in Section 20.3.2.28 of an ECMA-262 internal version):⁷

It first converts the given parameter x to its numeric value n using ToNumber. The remaining steps should be performed using n, but the specification writer of this section mistakenly used x instead of n in steps 3 and 4. This bug was introduced in ECMA-262 on September 11, 2020 and was later fixed by another contributor.

In addition, keeping a rapidly evolving language specification up to date and managing the many different language implementations that conform to the specification is challenging even with a large test suite. The three editors of ECMA-262 had to manually review new proposals and changes to the specification. In addition to Test262, various browsers maintain their own test suites, but they may still behave differently. Therefore, Ficarra,¹⁶ an editor of ECMA-262, said, “one of my primary goals has been to make the specification easier to consume for automated analysis tools.”

Academic Research into the CI Systems

We helped Ficarra achieve his goal in November 2022: each ECMA-262 pull request (PR) runs a type checker against the prose specification, and all new or changed tests in Test262 PRs are run using an interpreter extracted directly from the text of ECMA-262. For example, if one sends a PR of the Math.round function, the type checker will detect a bug and reject the PR. First, note that the parameter x can accept any JavaScript value: string, boolean, number, object, and so on. Applying ToNumber to x in step 1 converts x to a number or an exception. Exception cases are filtered out using the question mark operator, so n always points to a number. Because x is compared to several numbers with inequality operators on lines 3 and 4, the type checker reports them as type mismatch bugs because non-numeric values are not valid arguments for inequality operators. Whenever a language feature is added to ECMA-262, it must be accompanied by its corresponding tests in Test262, which now leverage interpreters extracted from ECMA-262, always checking for conformance to ECMA-262. These automated tools, heavily used in the continuous integration (CI) system of ECMA-262 and Test262, are based on a series of academic papers.

How have ideas from academia been integrated into real-world industry? How did researchers convince the TC39 committee to use their ideas?

The KAIST Programming Language Research Group (PLRG) has been researching JavaScript since 2011. Initially, we mainly formalized the semantics of the JavaScript language with various features, but now our research focuses on program analysis and bug finding in JavaScript applications. Our research problems are often motivated by real-world customers in companies such as Samsung Electronics and IBM. This work had been challenging, interesting, rewarding, and fun until TC39 decided in 2015 to release ECMA-262 annually. As the JavaScript language has evolved more rapidly, developing and maintaining JavaScript analysis tools has become increasingly difficult.

As the JavaScript language has evolved, developing and maintaining JavaScript analysis tools has become increasingly difficult.

In March 2019, Ph.D. candidate Jihyeok Park cautiously shared an outlandish idea. ECMA-262 had been released annually since 2015, but existing JavaScript analyzers, including our own, were still based on ES5, which was released in 2009. It is impossible to manually keep up with the changes in an 800-page specification every year. Then he realized something: the English phrases in the specification had common patterns. It might be possible to “parse” the English sentences and “compile” them into abstract algorithms in an intermediate language. We considered this a clever engineering hack, which could help us generate more tests for features of ECMA-262 that Test262 does not cover.

In essence, it was the primary enabler; the direct extraction of “mechanized specifications” from prose-written language specifications has opened the door to the automatic generation of language-manipulating tools. To bridge the gap between ECMA-262 and its implementations, ESMeta²¹ extracts mechanized specifications to automatically generate a variety of language-based tools from a given version of ECMA-262. It is based on several papers. JISET²⁸ extracts a mechanized specification from ECMA-262. A mechanized specification consists of two parts: a JavaScript parser constructed from the syntax written in a variant of the extended BNF (EBNF) notation, and functions in an intermediate representation (IR) compiled from abstract algorithms written in English for the language semantics. JEST²⁷ synthesizes conformance test programs and checks discrepancies between JavaScript engines and the specification. Using this tool, we detected 44 bugs in four engines (V8, GraalJS, QuickJS, and Moddable XS) and 27 bugs in ES2020. JSTAR²⁶ analyzed the types of English sentences in ECMA-262 and detected 93 type-related specification bugs, which were confirmed by TC39. JSAVER²⁵ automatically generates a JavaScript static analyzer from ECMA-262, which outperforms the state-of-the-art JavaScript static analyzers that were manually developed. The next section offers a description of the technical details behind them.

The direct extraction of “mechanized specifications” from prose-written language specifications has opened the door to the automatic generation of language-manipulating tools.

Because the papers presented various new techniques using mechanized specifications, we used their bug-finding capabilities to evaluate the effectiveness of the techniques. Thus, we submitted many bug reports to mainstream JavaScript engine developers and the TC39 committee for confirmation. They kindly confirmed the bugs and expressed a lot of curiosity. Then, the ECMA-262 editors invited us to a TC39 meeting.

The presentation was very well received. All the excitement from the TC39 committee and the detailed discussion can be found in the meeting note.¹³ After mutually exciting meetings with the TC39 committee, we decided to integrate JSTAR and JISET into the CI systems of ECMA-262 and Test262, respectively. Since these tools were prototype implementations to see their feasibility in academic publications, we reimplemented all the tools and rebranded them as ESMeta to make them practically available to all PRs in the ECMA-262 and Test262 repositories.

After the first meeting with ECMA-262 editors on Nov. 24, 2021, we gave a presentation at the TC39 meeting on Jan. 27, 2022. ESMeta was then integrated into ECMA-262’s CI system on Nov. 3, 2022¹² and Test262’s CI system on Nov. 25, 2022.⁹ This was about a year after the first meeting with the TC39 committee. This is how the initial outlandish idea and subsequent academic papers were integrated into real-world programming language development.

Technical Details

Researchers have proposed various approaches to help developers build correct JavaScript applications.^1,32

One approach is to formalize the JavaScript language semantics described in ECMA-262. Because ECMA-262 defines semantics in prose, it is sometimes ambiguous and contains bugs and infeasible behavior. Researchers have proposed formal specifications for JavaScript semantics to provide a solid foundation for JavaScript research. Maffeis et al.²² proposed a small-step operational semantics for ES3; Guha et al.¹⁸ used a desugaring process to develop λ_JS, a core calculus of ES3; and Park et al.²⁴ defined ES5 using the K framework.³⁰

Another approach is to analyze JavaScript programs to reason about their behavior or detect bugs and security vulnerabilities. WALA¹⁹ was initially developed for Java pointer analysis and has been extended to support more languages, including Android Java and JavaScript. TAJS²³ is a dataflow analysis for JavaScript that uses a model of ES3 and a partial model of ES5. It provides partial support for the latest ECMAScript language features with Babel,³ which compiles the latest features down to lower versions. SAFE²⁰ is a general analysis framework for JavaScript web applications. These are all open source projects for static analysis of JavaScript. In contrast, Jalangi³¹ is a general framework for JavaScript dynamic analyzers such as memory profilers and dynamic JIT-unfriendly code snippet detectors.

While most of the research on JavaScript is for ES3 and ES5, ECMA-262 has been released every year since 2015. Thus, manually updating the semantic formalizations and analysis implementations is tedious, labor-intensive, and error-prone.

To bridge the gap between the rapidly evolving ECMA-262 and its implementations, ESMeta generates various tools directly from ECMA-262. Figure 1 illustrates the overall structure of ESMeta. The first step is to extract a mechanized specification from an input ECMA-262 via JISET. Once a mechanized specification is available, it can be used to check the validity of ECMA-262. We can use JEST to synthesize new kinds of conformance tests and JSTAR to analyze the types of English phrases in the specification. Finally, we can use JSAVER to derive a static analyzer for a given version of ECMA-262. We will describe them in order.

val ArrayLiteral: List[Boolean] => LAParser[T] = memo {
   case List(Yield, Await) =>
     "[" ~ opt(Elision) ~ "]"        ^^ ArrayLiteral0 |
     "[" ~ ElementList(Yield,Await)
         ~ "]"                       ^^ ArrayLiteral1 |
     "[" ~ ElementList(Yield,Await)
         ~ "," ~ opt(Elision) ~ "]"  ^^ ArrayLiteral2
 }

syntax def ArrayLiteral[2].Evaluation(
     this, ElementList, Elision
   ) {
     let array = [! (ArrayCreate 0)]
     let nextIndex =
       [? (ElementList.ArrayAccumulation array 0)]
     if (! (= Elision absent))
       [? (Elision.ArrayAccumulation array nextIndex)]
     return array
   }

var x = { p: 42 };
        $verifyProperty(x, "p", {
            value: 42.0,      writable: true,
            enumerable: true, configurable: true
        });

Type Analysis of Specifications

Manually reviewing every specification update is inherently labor-intensive and error-prone, making ECMAScript vulnerable to specification bugs. Because the average number of updated steps of abstract algorithms between consecutive releases from ECMAScript 2016 to 2019 was 9,645.5,²⁸ manually checking for every update is a daunting task. Thus, TC39 pushed to add various manual annotations to the abstract algorithms to reduce specification bugs. First, it introduced two kinds of annotations: assertions, which indicate assumptions at specific points in abstract algorithms, and the prefixes ? and !, which indicate whether the execution of an abstract algorithm completes abruptly. For example, “Assert: Type(O) is Object” denotes that the variable O always has an Object value at the point of the assertion, and “? GetV(V , P)” denotes that the execution of GetV(V , P) can complete abruptly. These annotations help readers understand specifications clearly. Second, the committee decided to support type annotations for variables, parameters, and return values of abstract algorithms. However, manual annotations of any kind are laborious, prone to mistakes, and do not provide an automatic mechanism for detecting specification bugs.

Manual annotations of any kind are laborious, prone to mistakes, and do not provide an automatic mechanism for detecting specification bugs.

To alleviate this problem, we developed JSTAR,²⁶ which takes a mechanized JavaScript specification from JISET and performs type analysis of compiled functions using the specification types defined in ECMA-262. ECMA-262 contains not only JavaScript language types, but also specification types such as abstract syntax trees (ASTs), internal list-like structures, and internal records including environments, completions, and property descriptors. For records and AST types, we also defined their fields. We defined their type hierarchies based on subtype relations. The subtype relation between types is shown in Figure 2; a directed edge from τ′ to τ denotes a subtype relation (that is, τ′ <: τ), and the relation is reflexive and transitive. The subtype relation depends on the nominal types defined in ECMAScript. We extract the subtype relation for AST types from the JavaScript syntax. For example, consider the following syntax:

FormalParameter_{[?Yield, ?Await]} ] : BindingElement_{[?Yield, ?Await]} ]

Because the nonterminal BindingElement is the unique alternative of the production FormalParameter, we automatically extract the subtype relation: BindingElement <: FormalParameter. Using the subtype relation, the expression e : τ checks whether the evaluation result of e has type τ′ satisfying τ′ <: τ. These subtype relations help enhance the precision of type analysis by keeping track of the precise types of variables and expressions.

Using such type information, JSTAR performs type analysis and detects specification bugs using a bug detector consisting of four checkers: 1) reference checker, 2) arity checker, 3) assertion checker, and 4) operand checker. JSTAR also uses condition-based refinement for type analysis, which improves the precision of type analysis by using conditions on assertions and branches to eliminate infeasible parts. We evaluated JSTAR with all 864 versions in the official ECMAScript repository from 2018 to 2021. The evaluation showed that the refinement technique can reduce the number of false-positive bugs due to spurious types inferred by imprecise type analysis. JSTAR detected 14 type-related bugs in ES2021,⁸ which were confirmed by TC39.

Derivation of Static Analyzers

Finally, we developed JSAVER,²⁵ which automatically generates a JavaScript static analyzer from ECMA-262. First, JSAVER extracts definitional interpreters²⁹ from ECMA-262. A definitional interpreter provides a way to represent the language semantics of a defined language using its interpreter written in a defining language. We extract a JavaScript definitional interpreter from JISET. In the extracted definitional interpreter, the defined language is JavaScript, and the defining language is IR_ES. We then present meta-level static analysis, which uses the extracted interpreter to indirectly analyze JavaScript programs. Meta-level static analysis is an interpreter-based approach for static analysis of a defined language L₁ using the static analyzer of a defining-language L₂, as depicted in Figure 3. Since an L₁ interpreter is an L₂ program, we can indirectly analyze an L₁ program by taking the L₁ program as input and using the static analyzer of L₂ to analyze the interpreter. Thus, we developed a static analyzer of IR_ES for a meta-level static analysis of JavaScript and showed that it can indirectly analyze JavaScript programs effectively. We also presented ways to indirectly configure abstract domains and analysis sensitivities for JavaScript in the static analysis of IR_ES. First, we provide a method to configure abstract domains for JavaScript values and structures. Second, we present AST sensitivities to express analysis sensitivities for JavaScript, such as flow-sensitivity and k-callsite-sensitivity.

Figure 4 shows the analysis results of existing static analyzers (TAJS and SAFE) without and with Babel, and JSA_ES2021, the JavaScript static analyzer derived from ES2021 via JSAVER, for the applicable tests. In each chart, the x-axis represents the point in time when the tests were generated and the y-axis represents the number of tests generated before that point in time. The mark sound (green, filled) denotes a sound analysis, unsound (red, striped) denotes an unsound analysis, and error (white, blank) denotes an unexpected error. Figures 4(a) and 4(b) show that TAJS and SAFE analyzed most tests generated before 2015 in a sound way. However, the number of tests that cannot be soundly analyzed has been steadily increasing since 2015. As shown in Figures 4(d) and 4(e), Babel transpiles ES2015+ features to ES5.1 to mitigate this issue and increase the number of programs that TAJS and SAFE analyze soundly. However, TAJS and SAFE still failed to soundly analyze more than half of the Test262 test programs, while JSA_ES2021 succeeded in soundly analyzing all applicable test programs without the need for Babel. The figures show that JSAVER can reduce the burden of defining the abstract semantics of ES2015+ features for static analysis.

A Promising New Approach to Programming Language Development

Designing and implementing real-world programming languages is challenging. The ability to reason about program behavior often comes from a formal specification of the language’s semantics, but the time-consuming effort of formalizing the semantics often falls behind actual implementation. For example, Rust is actively developed by a large and diverse community of contributors and is used in real-world software such as the Linux kernel and Mozilla Firefox. However, it has not resolved soundness bugs reported years ago⁴ because its strong, static type system does not yet cover various language features and APIs. Applying the ESMeta approach to Rust can help efficiently generate machine-checkable proof sketches, especially with mechanized semantics extracted from mechanized specifications.

Along with formalizing the semantics of the language, it would be helpful to perform extensive testing of the semantics using implementations extracted from the mechanized specification. Watt et al.³⁵ presented two mechanizations of WebAssembly 1.0 and found bugs in it, but mechanization of WebAssembly 2.0 will still be quite time-consuming because the entire mechanization process is done manually. Applying the ESMeta approach to WebAssembly can reduce the burden of such manual mechanization.

A promising new approach to programming language development is to design languages with mechanized specifications from the beginning. For developers, mechanized specifications can be easier to understand than specifications in natural language because they are unambiguous and always executable. For non-developers, mechanized specifications can be translated into diverse, human-friendly natural languages. Furthermore, implementations and tools that are extracted directly from mechanized specifications are correct by construction.

A promising new approach to programming language development is to design languages with mechanized specifications from the beginning.

Designing a new programming language by writing a mechanized specification that correctly describes the language’s intended behavior can seem daunting, but it is possible because mechanized specifications allow us to create a variety of tools. For example, one can run the specification interactively. Figure 5 shows another ESMeta tool, the ECMAScript Double Debugger.²¹ This tool extends the interpreter extracted from ECMA-262 to help users understand how JavaScript programs are executed according to ECMA-262. It supports step-by-step execution of ECMA-262 abstract algorithms, line-by-line execution of JavaScript code, breakpoints by abstract algorithm name in ECMA-262, and visualization of ECMA-262 internal states. Language designers can use the debugger to run example code to debug their mechanized specifications. For instance, Verse introduced new features such as logical variables, equality constraints between variables, and choice that allows multiple alternatives. Describing the intended behavior precisely is cumbersome, but a double debugger can ease the burden on language designers.

Conclusion

JavaScript is the first programming language for which each change to its prose language specification is both “type checked” and also “tested” to identify bugs and inconsistencies. In this article, we presented our story of applying various ideas from academic papers to the continuous design and implementation process of the real-world programming language in the wild. As one of the reviewers of the JISET paper suggested, we believe that:

This is the right order to design and document languages: first the semantics, then the implementation and documentation, ideally generated from the semantics.

Acknowledgments

We would like to thank all members of the KAIST Programming Language Research Group (PLRG) for their collaboration, especially Jaemin Hong for his insightful feedback. This research was supported by National Research Foundation of Korea (NRF) (2022R1A2C200366011 and 2021R1A5A1021944), Institute for Information & communications Technology Promotion (IITP) grant funded by the Korea government (MSIT) (2022-0-00460 and 2023-2020-0-01819), and Samsung Electronics Co., Ltd (G01210570).