Nex is not an invention from nothing. Its structural vocabulary, its discipline of contracts, its type ideas, and its model of concurrency are each drawn from a body of earlier work. Even the form of this Definition — the separation of syntax from semantics, and of static from dynamic semantics — is itself inherited. This appendix gathers the principal sources.
The works below are those the body of the Definition appeals to by name. Each is the origin of an idea that Nex adopts:
- Design by Contract and the class structure, from Eiffel
- the conviction that a small, regular core scales further than a large feature set, from Scheme
- the discipline of types, from ML
- the axiomatic reading of preconditions and postconditions, from Hoare logic
- the rendezvous model of communicating processes, from CSP, by way of the goroutine-and-channel style of Go
- the method of formal language definition, from The Definition of Standard ML
- Ecma International. ECMA-367: Eiffel — Analysis, Design and Programming Language. 2nd edition. Ecma International, Geneva, 2006.
- The Go Authors. The Go Programming Language
Specification. Google. The source of the goroutine-and-channel model that
Nex’s
spawn,Channel, andselectfollow. - Hoare, C. A. R. “An Axiomatic Basis for Computer Programming.” Communications of the ACM, 12(10):576–580, 1969. The origin of the precondition / postcondition reasoning underlying Nex’s contracts.
- Hoare, C. A. R. “Communicating Sequential Processes.” Communications of the ACM, 21(8):666–677, 1978. Expanded as Communicating Sequential Processes, Prentice Hall International, 1985. The model of synchronous communication behind Chapter 6.
- Kelsey, R., Clinger, W., and Rees, J. (editors). Revised5 Report on the Algorithmic Language Scheme. 1998. The articulation of the small-core principle that Nex takes from Scheme.
- Meyer, Bertrand. Object-Oriented Software Construction. 2nd edition. Prentice Hall, Upper Saddle River, New Jersey, 1997. The statement of Design by Contract and of the Eiffel class and inheritance model, including the covariant redefinition rule from which Nex deliberately departs (Section 4.3).
- Milner, Robin. “A Theory of Type Polymorphism in Programming.” Journal of Computer and System Sciences, 17(3):348–375, 1978. The root of the type discipline that Nex inherits from ML.
- Milner, Robin; Tofte, Mads; Harper, Robert; and MacQueen, David. The Definition of Standard ML (Revised). The MIT Press, Cambridge, Massachusetts, 1997. The model, in spirit and in structure, for the present document: semantic objects, the judgement \(B \vdash \mathit{phrase} \Rightarrow A\), and the separation of static from dynamic semantics.
Beyond these named sources, this Definition is indebted to the Nex implementation itself: its grammar, its tree-walking interpreter, and its reference documentation. These remain the authoritative account of the language against which this document is to be checked (Section 1.3).