Designed for Correctness

Most modern languages are very good at telling you that a program is well-formed. They are far less interested in whether it is correct. A type checker confirms that you passed an Integer where an Integer was expected; it has nothing to say about whether the integer should have been positive, whether the account had sufficient balance, or whether the list was supposed to stay sorted. That gap — between “it compiles” and “it does what it promised” — is where most real defects live. Nex is built around closing it.

1Contracts as a language primitive, not a library

A contract is a precise, checkable statement of what a routine expects and what it guarantees. In Nex you write it directly in the declaration of the routine, not in a comment and not in a separate test file:

class Account
feature
  balance: Integer
create
  make() do balance := 0 end
feature
  deposit(amount: Integer)
    require
      positive: amount > 0
    do
      balance := balance + amount
    ensure
      grew: balance = old balance + amount
    end
end

A precondition (require), an implementation, and a postcondition (ensure) — one artifact.

The require block states the caller’s obligations; the ensure block states the routine’s guarantees. The keyword old refers to a value as it was on entry, so a postcondition can talk about change, not just final state. Classes carry invariant blocks for properties that must hold between calls, and loops carry variant clauses that must strictly decrease — a built-in proof that the loop terminates.

These are not assertions bolted on by a library. They are part of the grammar, and that distinction is the whole point. Because contracts are first-class, the language can do things a library never could:

Violations are precise and named. Calling deposit(-5) does not produce a generic stack trace; it reports Precondition violation: positive. The blame is assigned correctly — to the caller — and labelled with the exact clause that failed.
The pre-state is available. old balance is meaningful only because the runtime captures it before the body runs. A library assertion cannot reach back in time.
Contracts are the documentation. The signature plus its contract is the specification. It cannot drift out of date the way a comment can, because it is executed.
They compose with inheritance correctly — which is the subject of the next section, and the place where “a library could do this” finally breaks down completely.

A contract written in the language is an executable specification: the documentation, the test oracle, and the first responder in the debugger, all the same line of code.

2Liskov substitution, done right — and done automatically

The Liskov Substitution Principle says that an object of a subclass must be usable anywhere its parent is expected, without surprises. Stated as a rule about contracts, it is exact:

A subclass may weaken a precondition (accept more), never strengthen it. A caller who satisfied the parent must still be served.
A subclass may strengthen a postcondition (promise more), never weaken it. A caller who relied on the parent’s guarantee must still get it.
A subclass is bound by all of its ancestors’ invariants, plus its own.

Eiffel, where Design by Contract originates, asks you to opt into this with special syntax (require else, ensure then). Nex takes a stronger position: it makes substitutability the default and only behaviour, by combining contracts down the hierarchy automatically. When a method is resolved, its effective contract is computed as:

effective precondition = parent precondition or child precondition. The set of acceptable calls can only grow as you descend. You cannot accidentally narrow it.
effective postcondition = parent postcondition and child postcondition. Every guarantee an ancestor made is still enforced on the override.
effective invariant = the conjunction of every invariant from the root down.

The consequence is that you cannot write a subclass that quietly betrays its parent’s promises. Suppose someone overrides deposit with a buggy body and no postcondition of its own:

class BuggyAccount
inherit
  Account
feature
  deposit(amount: Integer)
    do
      balance := balance + amount + 1   -- wrong
    end
end

The override declares no ensure clause at all. It does not matter. The parent’s postcondition is part of the effective contract, so the call fails exactly where it should:

Error: Postcondition violation: grew

This is the difference between subtyping that is merely type-sound and subtyping that is behaviourally sound. A type checker would happily accept BuggyAccount — the signatures match. Nex rejects the behaviour, because the contract travels with the method. Inheritance stops being a place where guarantees leak away and becomes a place where they accumulate.

In Nex, a subclass can promise more and demand less, but never the reverse — and you get that guarantee without writing a single extra keyword.

3Interfaces you can trust: uniform access and command–query separation

Contracts describe what individual routines do. Two further principles, both built into how Nex is taught and designed, describe how a whole interface should behave — and they reinforce each other.

Uniform access

In Nex, reading a stored field and calling a computed method use identical syntax:

p.x                      -- reads a stored field
p.distance_from_origin   -- calls a computed method

The caller cannot tell, and does not need to tell, which is which. This is the Uniform Access Principle, and its payoff is representation independence: a class can turn a stored field into a computed one — or the reverse, caching for performance — without breaking a single line of calling code. The interface is a set of questions the object answers, not a list of how it happens to store its data today.

Command–query separation

Uniform access is only safe if asking a question never changes the answer. That is the second principle: a command changes an object’s state; a query reports something about it; and a well-designed routine does one or the other, not both.

Consider a counter whose “query” secretly mutates:

next_value(): Integer do
  value := value + 1   -- a question that changes the answer
  result := value
end

The name sounds like an observation, but every call advances the counter. A reader cannot tell from the call site whether obj.next_value is safe to evaluate twice. The disciplined design splits the two roles:

class Counter
private feature
  value: Integer
feature
  increment() do
    value := value + 1
  end
  current(): Integer do
    result := value
  end
end

Now increment is a command and current is a query, and the interface says exactly what happens. A caller can read current as many times as it likes without disturbing the object, and can advance the counter without pretending to ask a question.

Put the three ideas together and a coherent design philosophy appears. Command–query separation guarantees that queries are side-effect-free; uniform access then lets you treat any query as interchangeable with a stored value; and contracts pin down precisely what each command and query promises. A caller can read any feature without fear, reason about it locally, and depend only on its contract — never on its implementation. That is what “good interface design” means in concrete, mechanical terms, rather than as advice.

4A correctness-first language for learning

This is why Nex makes a good first language, and it is a deliberate inversion of how programming is usually taught. The conventional path introduces syntax first and correctness last — if at all — once a separate testing framework is bolted on much later. The implicit lesson is that getting code to run is the real work and reasoning about whether it is right is an optional, advanced topic.

Nex reverses the order. Stating what a routine requires and ensures is not an advanced technique here; it is how you write the routine in the first place. A learner is nudged, by the shape of the language, to ask the questions a good engineer asks before trusting any piece of code: What must be true for this to make sense? What will be true once it finishes? What never changes? Those questions are problem decomposition, interface design, and invariant-finding — the actual content of software engineering — and Nex puts them at the centre of the page instead of in an appendix.

The mainstream industrial languages cannot easily play this role, and not by accident: their complexity exists to serve the demands of their real users, and that complexity cannot simply be set aside for newcomers. A first language has a different job. Its job is to make good habits unavoidable, and good habits are exactly what a contract makes explicit.

5Small enough to understand

A correctness-first language only helps a learner who can actually reach the contracts — if the rest of the language stands in the way, the lesson never lands. Nex is built so that it does not. It was designed to be small enough to understand, disciplined enough to teach sound habits, and practical enough to support real programs. Four properties carry most of that weight, and each earns its place by removing an obstacle between a newcomer and the ideas.

A small core. The grammar is kept small enough that its semantics can be explained without hand-waving. New conveniences — extra operations, host integrations, whole libraries — live outside the language rather than arriving as fresh keywords, so the kernel never grows unintelligible by accumulation. A learner can hold the whole language in their head, and nothing in it is magic to be explained away "later."

Clear syntax. Nex reads like structured English rather than a thicket of symbols. Blocks open and close with words — do … end, feature, require, ensure — and the notation neither hides intent behind punctuation nor buries it under ceremony. A first language's syntax should get out of the way of the idea; this one does, erring toward neither the cryptic nor the verbose.

Static typing with inference. Types are checked before a program runs, so a mistake arrives as an explanation rather than as a crash partway through execution — the same early, localised feedback that makes contracts valuable. Annotations double as documentation of intent, yet in the REPL they are optional, so exploration stays light while finished code stays explicit.

Objects and functions, without friction. A student meets the two dominant styles of programming — object-oriented and functional — inside one coherent language, each used where it fits: a class may use a function internally, and a function may manipulate objects. Nex makes no ideological commitment to either, so a beginner learns concepts rather than tribal allegiances, and never pays a tax to move between them.

None of these is remarkable on its own — every language claims a clean syntax and a small core. What matters is the combination and what it is for: together they clear away the reasons a newcomer might stall before reaching the part of Nex that actually teaches engineering — the discipline of stating what code must do, and having the language check it.

6Why this matters even more in the age of generated code

Large language models have made it cheap to produce plausible code. They have done nothing to make it cheap to trust it. A model emits a function that looks right; the burden of deciding whether it actually meets its intent falls back on the human — and reading code to confirm intent is exactly the slow, error-prone task the model was supposed to relieve.

A Design-by-Contract language changes the shape of that problem, because a contract is a machine-checkable statement of intent that is separate from the implementation. That separation is precisely what generated code lacks and most needs:

The specification can be written independently of the code. A person — or a model acting as the specifier — states the require/ensure/invariant: the what. Any implementation, hand-written or generated, is then checked against it the moment it runs. The contract becomes the target the generator must hit and the grader that says whether it did.
Failures are localised and named. When generated code is wrong, a violated postcondition points at the offending routine and the specific clause it broke — far more actionable for an automated repair loop than a distant, mislabelled crash.
Contracts are superb context for a model reading code. They state intent more precisely than comments and cannot have rotted, so a contract-annotated codebase is one a model can extend with far less guesswork about what each piece is for.

It is worth being precise about the limits. Runtime contracts are not proofs; they catch a violation when the offending path is actually exercised, not before. But that is exactly the verification layer that generated software most conspicuously lacks today — an executable, checkable boundary around each unit of intent. In a world where more and more code is written by something that does not understand what it wrote, a language whose central feature is stating and checking what code is supposed to do is not a historical curiosity. It is ahead of the problem.

7The bet

Nex is not trying to out-compete Rust on memory safety or Haskell on purity or TypeScript on ecosystem. Those are battles fought on other languages’ terms. Its bet is narrower and, I think, more durable: that the foundation of good software — whether you are a student learning to think rigorously, an engineer designing an interface meant to outlive its first implementation, or a system supervising code that a machine produced — is the ability to state what a program must do and have that statement checked. Nex makes that the first thing you learn and the last thing you can forget.

→ Nex in 15 Minutes → Syntax Postcards → Programming with Nex (book)