Introduction — The Definition of Nex

A precise description of a programming language is a prerequisite for its implementation and for its use. This document is such a description for Nex: a formal account of both the grammar and the meaning of the language.

A language description can take many forms. The most common is the reference manual: a careful narrative of what each construction does, usually backed by a grammar in Backus–Naur form. That is enough for many purposes, and Nex has such a manual. But a reference manual is ill-suited to the reader who must implement the language, who wishes to state laws for the equivalence of programs, or who wants to reason about a program with mathematical rigour. For those readers a different kind of document is needed, in which the meaning of a program is not described but defined.

This Definition aims to be that document. It does not replace the tutorial or the reference; it underwrites them. Where the tutorial says what a construct is for, the Definition says what it is.

1.1Nex

Nex is a small object-oriented language with first-class functions, designed to keep the discipline of software engineering visible in ordinary code. It draws its structural vocabulary—classes, features, inheritance, and contracts—from Eiffel; its conviction that a small, regular core scales further than a large feature set from Scheme; the discipline of static, soundness-minded typing—checked before a program runs and set down, like this Definition, in inference rules—from ML; and its concurrency model—lightweight tasks communicating over channels—from CSP and its descendants. What Nex takes from ML is this discipline, not the type algebra of ML proper: the type structure itself—nominal classes related by inheritance and conformance, with bounded generics—is Eiffel's, and Nex has neither Hindley–Milner inference nor structural typing.

Four commitments shape the language, and the tension between them gives it its character.

Correctness is part of ordinary programming. Preconditions, postconditions, and class invariants are written in the program itself, checked as it runs, and reported by name when they fail. They are not a separate proof obligation in another file; they are Design by Contract, carried forward from Eiffel.
Readability must survive growth. A language that is clean at ten lines and illegible at ten thousand has solved the wrong problem. The core grammar is kept small enough that its meaning can be stated without hand-waving—which is precisely what makes a document like this one possible.
Objects and functions cooperate. Classes, inheritance, and contracts model the stateful parts of a system; pure functions and immutable values handle the rest. Neither is treated as the privileged paradigm.
Theory shows up as design, not as notation. The contract system has roots in Hoare logic, the static typing discipline in ML, the concurrency model in CSP. None of this is required of the programmer. The theory pays for itself in the regularity of the surface.

It is the third and fourth commitments that make Nex worth defining formally, and the second that makes it feasible.

1.2The Form of the Definition

Every programming language presents its own conceptual view of computation. This view is indicated by the words the language uses for its phrase classes—class, feature, contract, task, channel—but those words also have abstract counterparts, which are what people really have in mind when they use the language. These abstract counterparts we call semantic objects; it is they, not the syntax, that carry the character of a language. A definition of Nex must therefore be given in terms of such objects.

Following the tradition established by The Definition of Standard ML, we factor the task in two ways.

First, we separate syntax from semantics. Chapters 2 and 3 give the grammar: the rules that decide which strings of characters are Nex programs. The remaining chapters give the meaning of the programs so admitted.

Second, we separate the static semantics from the dynamic semantics. The static semantics (Chapter 4) describes what can be determined about a program before it runs—the types of its expressions, the conformance of its classes, the well-formedness of its contracts. The dynamic semantics (Chapter 5) describes what happens when the program is evaluated. This factoring mirrors the implementation, which checks a program statically and then either interprets or compiles it; and it mirrors the experience of the programmer, for whom a type error and a contract violation are events of two quite different kinds.

The shape of an assertion The keystone of the method is a certain kind of assertion about evaluation. It takes the form \[ B \vdash \mathit{phrase} \Rightarrow A \] and may be read: against the background \(B\), the phrase evaluates to \(A\). The background \(B\) is itself a semantic object—a distillation of the meanings established by earlier phrases (the classes in scope, the variables bound, the current object). In the static semantics \(A\) is a type and \(B\) is a collection of typing assumptions; in the dynamic semantics \(A\) is a value and \(B\) is a collection of bindings. The same shape of rule serves both.

1.3The Status of the Interpreter

Nex is defined here in mathematical notation that is independent of any implementation. But Nex also has a reference implementation: a tree-walking interpreter that reads the abstract syntax and evaluates it directly. That interpreter is, by the project’s own convention, the authoritative statement of what the language means; the bytecode and JavaScript back ends are correct exactly when they agree with it.

This Definition and that interpreter are intended to describe the same language. Where they agree, the Definition explains the interpreter and the interpreter exhibits the Definition. Where they disagree, one of them is in error, and the disagreement is a defect to be repaired rather than a matter of taste. The Definition does not silently extend the language; if it appears to, that is a bug in the Definition.

1.4How to Read This Document

The reader who wants only the grammar may read Chapters 2 and 3 and stop. The reader implementing a checker will want Chapter 4; the one implementing an evaluator, Chapter 5. The appendices collect the full grammar (Appendix A), the classes and values that exist before any user code is loaded (Appendix B, the standard environment), and the derived forms—surface conveniences explained by translation into a smaller bare language (Appendix C).

Throughout, a few notational conventions are observed. Nex source text is set in a monospaced face: class, require, spawn. Nonterminals of the grammar are set in slanted type: exp, dec, ty. Semantic objects and the judgements relating them are set in mathematics. The symbol \(\Rightarrow\) is reserved for evaluation; \(\vdash\) for “elaborates” or “evaluates” in a context; and \(\preceq\) for the conformance relation between types introduced in Chapter 4.