DEV Community

Vijay Mathew
Vijay Mathew

Posted on AI-assisted

Nex: write code that keeps its promises!

#showdev #ai #programming #softwareengineering

Code generation has become cheap. Ask a model for a function and you get one that looks right in seconds. Deciding whether it is right still takes you just as long as it always did.

Most languages don't help much with that. A type checker tells you that you passed an Integer where an Integer was expected. It has nothing to say about whether that integer should have been positive, or whether the account had enough money before withdraw ran.

I've been building Nex, a small language that closes part of that gap. Every routine can state what it requires and what it guarantees, and Nex checks those promises each time the code runs. Nex is open source (MPL-2.0) and runs on the JVM. This post is a short tour.

A bug nobody notices

Here's a wallet with no contracts:

class Wallet
feature
  money: Real
  spend(amount: Real) do
    this.money := money - amount
  end
create
  with_balance(amount: Real) do
    money := amount
  end
end

let w := create Wallet.with_balance(10.2)
w.spend(20.0)
print(w.money)   -- -9.8
Enter fullscreen mode Exit fullscreen mode

The balance is now negative and the program keeps running with a value that shouldn't exist. The bug will show up later, after enough damage is done.

The same wallet, with its promises written down 

class Wallet
feature
  money: Real
  spend(amount: Real)
  require
    non_negative_amount: amount >= 0.0
    enough: amount <= money
  do
    this.money := money - amount
  ensure
    decreased: money = old money - amount
  end
create
  with_balance(amount: Real) do
    money := amount
  end
invariant
  never_negative: money >= 0.0
end
Enter fullscreen mode Exit fullscreen mode

Three kinds of promise appear here:

  • require is the caller's obligation. Spending more than you have is a bug in the code that called spend.
  • ensure is the routine's obligation. old money is the value on entry, so the postcondition can describe the change, not just the final state.
  • invariant must hold for every Wallet, after creation and before and after every call from outside.

Now the same call fails immediately, at the point where things went wrong, and the error names the clause:

nex> w.spend(20.0)
Error: Precondition violation: enough
Enter fullscreen mode Exit fullscreen mode

And a wallet can't even start out broken:

nex> create Wallet.with_balance(-10.0)
Error: Class invariant violation: never_negative
Enter fullscreen mode Exit fullscreen mode

These aren't assertions from a library. They are part of the grammar, which is why old can reach back to the value on entry. It's also why the contract can be the documentation: nex doc extracts signatures and contracts into a reference that can't drift from the code, because it's generated from it.

Write the spec, let someone else write the code

This is the part that matters most with AI in the picture. A deferred class (an abstract class, in most languages) can state a contract without any implementation:

deferred class Discount
feature
  apply(price: Real): Real
    note "The price after the discount."
  require
    non_negative_price: price >= 0.0
  deferred
  ensure
    never_more: result <= price
    never_negative: result >= 0.0
  end
end
Enter fullscreen mode Exit fullscreen mode

That's the specification: a discount never raises the price and never takes it below zero. It says nothing about how to compute it. Ask a model for a flat discount and you might get this:

class Flat_Off inherit Discount
create
  make(a: Real) do
    amount := a
  end
feature
  amount: Real
  apply(price: Real): Real do
    result := price - amount
  end
end
Enter fullscreen mode Exit fullscreen mode

It doesn't repeat a single clause, and it doesn't have to. In Nex, an implementation inherits every contract of the routine it implements, automatically. It works for the obvious test:

nex> create Flat_Off.make(10.0).apply(50.0)
40.0
Enter fullscreen mode Exit fullscreen mode

And it fails the first time the discount is bigger than the price:

nex> create Flat_Off.make(10.0).apply(5.0)
Error: Postcondition violation: never_negative
Enter fullscreen mode Exit fullscreen mode

A percentage discount configured at 150% fails the same way. Configured at -10%, it fails never_more. The spec is the target the implementation has to hit, and the check that tells you whether it did. Whoever wrote the implementation, a person or a model, gets caught the same way.

Inheritance works like this throughout Nex. A subclass can accept more and promise more, but never the reverse. Preconditions are combined with or and postconditions and invariants with and, so an override can't quietly break a promise its parent made.

I wrote about where this leads in When Code Is Cheap, Design the Promises. It covers how specifications and documentation change when code is cheap to generate. It also covers how to track the changes that matter as the code evolves: changes to what it promises, not just changes to the code itself.

"Isn't this just Eiffel?"

Nex owes a lot to Eiffel, where Design by Contract comes from, and the syntax shows it. Here are the main differences:

  • Contract inheritance is automatic. Eiffel asks you to opt in with require else and ensure then. In Nex, the safe combination is the only behaviour.
  • A small core. The grammar is small enough to learn in full. Libraries and host integrations live outside the language, so it doesn't grow a keyword for every feature.
  • Objects and functions together. Classes and inheritance sit beside first-class functions, so you can use whichever fits.
  • The JVM. Nex compiles a program to a single jar that runs anywhere Java does, and it can call Java libraries.

"Why not Java with assertions?"

You can get part of the way there, but it takes discipline. Java's assert is off unless you pass -ea. There's no old, so every postcondition about change needs local variables captured by hand. There are no class invariants, so the check has to be repeated at the end of every public method. And nothing makes a subclass honour its parent's contract.

Classes and their Contracts puts the same class side by side in Java and Nex.

What Nex isn't

Runtime contracts aren't proofs. A contract catches a broken promise when the code path that breaks it runs. A path no test or user exercises can still be wrong. In short: you state what a program must do, and Nex checks it.

It's at version 0.6.7, so the language can still change between releases. The tooling that exists today:

  • a REPL
  • a compiler to standalone jars
  • a formatter
  • nex doc
  • a language server, with a VS Code extension and an Emacs mode

The essay Designed for Correctness explains the design choices in more depth, including why contracts make Nex a good first language for teaching software engineering in the age of Generative AI.

Try it

You need Java 17 or later. On Linux and macOS:

bash <(curl -fsSL https://raw.githubusercontent.com/vijaymathew/nex/main/bootstrap-install.sh) jvm --install-deps
Enter fullscreen mode Exit fullscreen mode

Windows, user-local installs and building from source are covered on the install page. Then run nex to open the REPL.

Where to go next:

I'd like to hear what you think, especially from anyone who has tried Design by Contract in another language. What made it stick, or made you drop it?

Top comments (2)

Collapse
 
alexshev profile image
Alex Shev •

“Keeps its promises” is a good bar because it shifts the question from whether code runs to whether its observable contract survives change. I’d make those promises executable where possible: examples as tests, explicit failure behavior, and a small trace from requirement to verification. That gives maintainers something sturdier than intent to preserve.

Collapse
 
vijaymathew profile image
Vijay Mathew •

Yes we are talking about "executable promises". Some thoughts around how to make this methodology part of practical software design is covered in this blog post: schemer.in/nex/blog/when-code-is-c...