I find coding assistants compelling. They are extraordinary tools, genuinely transformational and I use them daily, and I’m interested in what becomes possible as they continue to get better. I’m also a CTO. At some point I have to be willing to sign off on the software we build. Sometimes directly, sometimes through the people and processes I’m responsible for.

Those two positions aren’t contradictory. But they do create a tension.

I can be impressed by an implementation without having sufficient grounds to approve it. I can believe these tools are enormously useful while still asking what, exactly, gives me confidence in their output. The fact that a model wrote the code doesn’t make that question go away. Nor does having another model tell me that the code looks good.

That’s the starting point for Onus: a programming language, and the development environment around it, built to explore a different basis for trusting generated implementations.

The compiler is already written in Onus. The workbench comes next.

The problem isn’t just whether the code is right

There are two different questions involved in approving a change.

Does the implementation satisfy its requirements?

And are those requirements sufficient for the system we intend to operate?

Code review often conflates the two. Reading an implementation helps us find mistakes, but it also helps us discover requirements nobody wrote down. We notice that something should be authorised, that a retry could repeat a payment, or that a seemingly innocent operation could become very expensive.

That is valuable engineering work and it was hard even before code started being generated at AI speed. My concern is what happens when the volume of generated implementation grows faster than our ability to do it.

We can respond with better tests, more automation, more selective review and better coding assistants. I expect all of those to matter. But I’m interested in a more fundamental question:

Can we change the thing a human has to review?

Nobody understands every line of a substantial production system today. We already rely on abstractions, interfaces, tools and other people’s judgement. I’m not proposing that we stop doing that.

I’m asking whether the boundary between what we inspect and what we trust can become more explicit—and more mechanically enforceable.

An instruction is not a constraint

Consider a reporting function that must never modify the database. We can put that rule in a ticket, a conventions document or a prompt. We can ask a reviewer to remember it. All of those communicate intent.

In Onus, we can also make it part of the function’s interface:

pub fn monthly_totals(db: sql.Db[ReadOnly], year: Int)
  -> Result[List[MonthlyTotal], sql.Error] may sql.read, alloc

The database capability is read-only. The declared effects permit database reads and allocation, not writes. Those restrictions apply through the functions it calls; moving a write into a helper doesn’t hide it from the compiler. This is the reporting example on the Onus site.

Suppose a model decides to record each report run by inserting a row into an audit table. That might be a perfectly reasonable feature. It is nevertheless outside the authority granted to this function.

The important question is no longer whether the model remembered the instruction. The proposed implementation crosses a boundary the compiler can reject.

Perhaps we decide the report should acquire write access. Perhaps we put the logging somewhere else. Either way, changing the boundary is a decision, not an incidental detail buried in generated code.

That separation also governs Onus’s regeneration loop. The model can revise implementations, but it cannot make them acceptable by weakening the contracts, widening the permitted effects or inserting a new assumption. It can propose such a change for a human to consider; it cannot silently award itself permission.

This is the division of responsibility I’m trying to establish: freedom to implement within agreed constraints, not freedom to redefine those constraints when implementation becomes inconvenient.

Permissions aren’t behaviour

Of course, a reporting function can be read-only and still return complete nonsense.

Restricting what code may do is not the same as establishing that it does the right thing. Onus also has behavioural contracts: preconditions, postconditions and invariants that create obligations for the checker.

But there is an important trap here.

Imagine specifying a sorting function by requiring that its result is sorted. An implementation that always returns an empty list satisfies that requirement. The result is indeed sorted. It just isn’t a useful implementation of the function we intended.

We also needed to say that the result contains the original elements, with their multiplicities preserved. The proof wasn’t wrong. The specification was inadequate.

That distinction is central to Onus. I’m not expecting the compiler to infer all the things I meant but failed to express. I want it to establish the properties I actually specified, and make clear what kind of evidence supports them.

The human still has a difficult job: deciding whether those properties are the right ones.

Contracts are code too. They can be subtle, incomplete and wrong. Moving complexity from a function body into an equally difficult specification would not, by itself, be progress.

The bet is that the properties we care about can often be expressed more clearly, reviewed more economically and retained across many different implementations.

That is a hypothesis to test, not a benefit I get merely by adding an ensures clause.

Proof, checking and assumption are different things

A green build is not a sufficiently detailed account of why something should be trusted.

Onus records obligations in a ledger, distinguishing those established statically, those checked at runtime and those accepted through explicit assumptions. The distinction matters: a runtime check can detect a violation, but it is not a proof that the violation will never occur. An assumption is a dependency on something the checker has not established.

These are not three interchangeable ways of saying “safe”.

For example, the checkout example includes an asserted idempotency claim that ultimately depends, in part, on a payment provider’s promise to deduplicate requests. The compiler tracks the claim and the assumptions supporting it. It does not prove the behaviour of the external payment provider.

That is useful precisely because it refuses to conceal where trust enters the system.

As a reviewer, I might accept an external guarantee under certain conditions. I might require evidence that we exercised it against a test environment. I might reject it for a particularly sensitive operation.

But I need to know that I am making that judgement.

I also need to understand its limits. Testing a provider’s behaviour gives me evidence about the cases tested. It doesn’t transform the provider’s promise into a universal theorem. Detecting an invalid state after an external side effect doesn’t necessarily undo that side effect.

The ledger is intended to support those distinctions, not flatten them into a reassuring badge.

What the human reviews

An individual function is only part of the picture. For requirements that apply across an operation, Onus has path declarations: constraints checked over the functions reachable from an entry point. These can bound effects, require claims and restrict which assumptions are acceptable.

The workbench is where I want those pieces to become a useful review experience.

Its inputs are compiler-produced interfaces, obligation records and path reports. The design is deliberately not another model reading the implementation and producing a plausible explanation. The review tool renders the evidence produced by the checking machinery.

I want a reviewer to see what changed in the terms under which an operation can be accepted. Does it need more authority? Has a behavioural promise weakened? Does something previously proved now require a runtime check? Has an external assumption been introduced? The interface and ledger comparisons are designed to expose those changes.

Those questions are much closer to the decisions I need to make as a CTO than “does this large diff look reasonable?”

They don’t replace judgement. They give judgement a more explicit object.

There is nothing new about contracts, effect systems, capabilities or formal verification individually. Onus draws on existing work in all of those areas. The experiment is in how they fit together around model-written implementations and human approval.

The language is necessary because the review surface needs something enforceable underneath it. The workbench matters because technically sound evidence that a person cannot understand or use is not enough.

Delete the implementation and see what survives

One way to investigate the premise is to deliberately discard implementations.

Onus’s regeneration audit removes bodies from the model’s context and asks it to rebuild them from their interfaces. The intention is to expose behaviour that depended on knowledge held only in the previous implementation.

Suppose the replacement satisfies every stated contract, yet we reject it because it behaves differently in a way that matters.

Perhaps it changes ordering that callers relied on. Perhaps it handles an edge case differently. Perhaps it is functionally correct but operationally too expensive.

We have found something important: our specification did not describe everything we needed to preserve.

That gives us a choice. We can capture the missing requirement, retain another form of evidence for it, or acknowledge that this part of the system still requires implementation review.

A successful regeneration doesn’t prove the specification is complete, either. Two implementations can share the same blind spot. A model may reproduce a convention because it is familiar, not because the interface requires it.

Regeneration is a way to challenge the specification. It is not a certificate of completeness.

Not reading the body is not the success criterion

I am interested in how often I need to open an implementation, and especially why.

If I open one to understand a permission boundary, perhaps the interface is missing something. If I open it to investigate performance, perhaps I need different evidence. If I open it because the report is confusing, that may be a workbench problem rather than a language problem.

But I could also stop opening implementations because the tool made me overconfident.

That would be failure, even if the body-open metric looked excellent.

The harder test is whether I can make good decisions with the evidence available: approve acceptable implementations, reject unacceptable ones, and recognise when the specification itself is insufficient.

That means deliberately looking for implementations which satisfy the stated claims but fail the intended job. It means noticing requirements discovered during operation, not just during review. It means accounting for the time spent writing and maintaining contracts, rather than counting only the time saved reading bodies.

I’m interested in less implementation review where it is justified—not less scrutiny.

The compiler is already written in Onus

The Onus compiler is now written in Onus.

That matters because a compiler is not an example chosen to make a language feature look good. It is a substantial piece of software with its own requirements, complexity and opportunities to get things wrong.

Next, I’ll be building the workbench in Onus.

These are related but different tests. Writing the compiler exercises the language. Building and using the workbench will test the development model: whether the evidence Onus produces is enough to support decisions I’m prepared to stand behind.

The first milestone doesn’t establish the second. A compiler written in Onus isn’t, by itself, proof that the checking machinery is sound, that the contracts capture everything important, or that implementation review can safely be reduced.

But it gives the experiment something substantial to work with.

As I build the workbench, I want to examine the decisions I make. What evidence was enough to approve a change? What made me inspect an implementation? What requirement did I discover only after running the software? Where did a perfectly satisfied contract turn out to describe the wrong thing?

The important result won’t be that I managed to avoid reading code. It will be whether I could make a defensible decision without reading it—and whether that decision held up afterwards.

I don’t yet know how broadly that will work. Finding out is the point.

I’m not building Onus because I dislike coding assistants. I’m building it because I find them compelling, and I want a development process that takes their capabilities—and our responsibilities—seriously.

The model can write the implementation. I still need grounds to sign it off.