On the first page of my first programming book, I met this:
x = x + 1
The symbols were familiar; the mathematics was not. At that time, in that country, computers were large machines “somewhere there,” and there was nobody nearby to ask. Eventually I learned that this was assignment, not an equation. I had been wrong about needing another mathematics. Not completely wrong.
A formula with decisions missing
My first serious program came from an unpublished article. It involved a complicated formula, with special functions, some linear algebra, and a convergent series. It was part of ongoing research, so what the program needed to do could change along the way.
I no longer remember the particular traps. I remember the rhythm: alter one thing, wait, alter another, and never quite know whether the work was converging or merely changing shape.
The machine was an IBM 370, fed with punched cards. On a good day I could get three runs. A first attempt that almost worked became a few months of small corrections: adjust a condition, wait, examine the printout, try again.
I was trained as a theoretical physicist and mathematician. In that profession, an error in an equation is disqualifying. I had expected to understand the calculation and write a correct program. Instead, I had written something with bugs, and was discovering what it should have been through successive repairs. The very existence of those bugs was hard to accept. Each correction fixed something, but left me wondering what entitled me to believe the next run would be right.
Three runs a day made it slow. The worse part was having to discover the program's meaning by repairing it.
Then another surprise arrived. After enough time had passed, I could no longer follow my own program. I could read each line, but not the reason the lines were arranged that way. Altering it felt less safe than writing it again.
The cards had preserved the instructions. The reason for the instructions had escaped.
What a programming language is really buying us
That experience changed what I thought a programming language was for. Saving keystrokes is pleasant. Keeping the shape of an idea while leaving machinery out of sight is more important.
Machine code tells a processor exactly what to do, but the idea behind it is hard to see. Assembly gives the operations names. Higher-level languages let us name a calculation, a repeated action, a kind of thing, a boundary. Strong types let us say, in effect, “that value has no business here.” Each step makes a bargain: the machine takes over some machinery and the programmer gets a description they can still recognize.
FORTRAN let a numerical calculation keep something of the shape of the formula on paper. That was an enormous gain: the compiler could arrange the machine instructions while the author could still recognize the calculation. But the shape of a formula does not preserve every reason for choosing an algorithm. My months of corrections had left those reasons scattered among conditions and jumps.
Types can carry some of this lost meaning. If account identifiers and organization identifiers are distinct types, the checker can reject a mix-up before the program runs. A rule that once depended on everyone remembering a convention becomes part of the language the machine understands. Yet knowing that a function accepts an organization identifier says little about whether it leaves every other organization alone. We have named the things; we still need to describe what may happen to them.
Most of us accept this bargain gladly. In Python, I do not trace every piece of memory as it is allocated and released. I trust the interpreter, yet I still feel responsible for the application. I chose its behaviour. I can point to the rule it is meant to obey.
Now imagine a product manager saying, “Anyone with an invitation may join the free plan.” Everyone in the room may nod. Then the questions arrive. Does the invitation expire? Can it be revoked? Is it held by a person or an organization? What if that organization already pays? Those are not edge cases waiting politely at the edge. They are the policy. The sentence was useful because it postponed them, until somebody had to build the thing.
Much of software work is exactly this: opening up the decisions hidden in a sentence that initially sounded settled.
How much fits inside a formula
Find a quantity which, multiplied by itself and then by a first known quantity, added to its product with a second known quantity, and then to a third, gives zero. We have barely stated the problem, and already there is a small procession of operations to keep in mind.
In school, we learned a shorter way:
ax2 + bx + c = 0.
For someone who knows the conventions, the expression has a recognizable shape. We see a familiar problem, perhaps recall a method, without spelling out each operation. Prose makes us trudge through what notation can put in front of the eye at once.
The formula earns its brevity from a shared education. Its symbols are partly instructions, partly reminders of patterns we have learned. Remove that shared background and the missing paragraphs return. A mathematician recognizes many of the unstated conditions almost before noticing that there was anything to ask.
Carrying out the calculation requires us to unpack what is relevant: choose a method, arrange the operations, account for the conditions under which they work. The distance between a value and a way of obtaining it can be considerable.
A good programming language helps us make the resulting calculation readable. But even ideally written code does not automatically restore all those missing paragraphs. We can follow what the program does and still have to reconstruct the assumptions that make it work.
Before there was a convenient second chance
Readable code lets us follow a calculation. But how do we establish that the program does what we intend? And when we change it, how do we know that our reasons for trusting it still hold?
This was the source of the frustration I described earlier: each correction fixed something, but left me unsure why I should trust the program as a whole.
The calculation was not enough. We needed mathematics whose subject was the program, not the quantities it calculated.
Edsger Dijkstra approached programming as a mathematical activity: state the properties a program must satisfy, make its assumptions explicit, and develop the program while preserving those properties. A future reader should not have to reconstruct all of the original author's thoughts from control flow and variable names. Some of the essential argument should remain explicit, available to be checked without relying on the author's memory or a few successful runs.
Dijkstra later recalled writing programs when the machine on which they would run was not even finished. There was no easy rhythm of run, fail, patch, repeat. The program had to make sense before it could be tried.
An invariant gives such reasoning something to hold on to: a property that must remain true while the state changes. Establish it at the beginning, then show that each step preserves it. When we change the program, we have something more precise to ask than whether it still seems to work: does the argument still hold?
Martin-Löf's type theory offers a way to make arguments about programs checkable by a computer. A type can require more than a particular kind of result; it can require evidence that the result satisfies a stated property. The reasoning can become part of what we write and what the machine checks.
For years this sounded like a concern reserved for rare, grave software. It no longer does.
The old gap, with an AI on the other side
AI coding agents make this gap painfully easy to see.
Ask one to implement “anyone with an invitation may join the free plan,” and it can rapidly create tables, handlers, screens, and tests. It may make many good decisions. But which answer will it choose to the questions hidden inside the sentence? It cannot discover an intention that was never fully expressed.
The question is not only whether an agent can write code we trust. We can hand it much of the how, as we hand compilers and interpreters details we no longer want to carry in our heads. The difficult part is the what: saying what we mean without reducing intent to a plausible blur.
The comparison has a catch. A compiler starts from an agreed language with defined semantics. An agent often has to infer the agreement. It may decide that an invitation belongs to an account, carry that decision through the database and interface, and write passing tests. The pieces can agree with one another and still disagree with the person who asked for the feature.
We usually answer with requirements in ordinary language and code review. We need both. They do not close the gap. A fluent requirement may still hide a policy decision, and a plausible implementation may faithfully realize the wrong interpretation. Reading unfamiliar code, now often written by a non-human, is not magically easier than writing it.
The agent's new freedom makes an old discipline more valuable. Keep important decisions somewhere shorter than the implementation, clearer than a pile of tickets, and unforgiving enough to expose the question nobody asked.
Giving the intention a home
At Yovico, we are trying a modest version of this idea. The product lets people bring together AI advisors to rehearse a board meeting, stress-test a strategy, or conduct customer-discovery interviews with AI personas. Turning intentions into coordinated machine behaviour is our daily work.
Suppose a requirement says subscriptions belong to organizations. One backend handler reads a plan from the user account. A frontend component shows one “current plan,” although the user belongs to several organizations. Every local decision may look reasonable, while the system as a whole no longer has one coherent meaning.
If code is treated as the final authority, a bug quietly joins the product definition until somebody spots it. Then intent has to be excavated from queries, handlers, screens, and old accidents.
Alongside the code and tests, we keep a formal specification of the central rules of the product. It gives us a place to state what belongs to an organization, what an account may do, and which relationships an operation must preserve, independently of any particular implementation.
When code disagrees with that model, the discrepancy is a defect to resolve. Changing the model is an explicit decision to change the product. Instead of asking what one handler happens to do, we can ask what should hold in every valid state.
The trouble with ordinary nouns
Writing such a specification quickly brings us back to ordinary words. Consider “the subscription is active.” Does that mean money remains owed, renewal will take place, or access is granted? A past-due subscription may still represent a debt while granting no paid functionality. Cancellation can stop renewal while leaving an already purchased period of access intact. One Boolean called isActive cannot carry all those meanings. Separate definitions of charging and entitling make us say which one we mean.
Ownership requires the same care. In our model, identity belongs to an account; billing and governance belong at the organization level; operational data belongs to a workspace. A person in three organizations can have three different sets of entitlements. Putting them on one Profile page does not turn them into one “account plan.”
These are product decisions before they are programming decisions. A formal model forces us to decide what each concept means, where it belongs, and how it may change. The useful discovery is often that a familiar noun had been concealing a meeting we had never held.
What we use Agda for
We write the model in Agda, a dependently typed programming language and proof assistant built on an extension of Martin-Löf's type theory. We use it to discover whether the concepts of a product fit together: whether every transition is defined, whether a refused request leaves the state unchanged, and whether policies that look reasonable separately remain consistent when combined.
Its data types describe the states and events the model admits. Its functions define when an action is allowed, what changes when it happens, and what constitutes a refusal. Those definitions must cover every admitted input. We can then state and prove laws about them: removing someone from one organization, for example, must preserve the state of unrelated organizations.
The checker asks us to supply the argument for such a law. It is not enough to give the operation a reassuring name or to show a few cases in which it behaves as intended. This is where the reasoning we wanted to preserve becomes part of the work itself.
This is nearer to application design than to proving a theorem or checking a numerical algorithm. We are using a proof assistant to help decide what our product means. Most of the mathematics it could perform is beside the point.
Why Agda?
There are dedicated specification frameworks for describing state machines, exploring reachable states, solving constraints, and checking properties over time. Their specialization can be an advantage: the framework supplies a vocabulary and tools suited to the questions it was designed to answer.
We chose Agda for the room it leaves us to formulate further questions. Domain concepts, executable definitions, propositions, and proofs inhabit one extensible language. We can begin by describing which actions are allowed, then state relationships between those actions, then ask what remains true through a sequence of them. We can introduce the concepts those arguments need as part of the model.
That matters in work where the questions change as we understand the product better. A model that begins with accounts and subscriptions may later need a more careful account of authority or isolation. We want to preserve what we have already expressed while developing the language needed for the next problem.
Other proof assistants can serve this purpose too. Agda appealed to us because of its direct programming-language style: definitions and the arguments about them can be developed together. More demanding properties still take work to formulate and prove. The attraction is being able to continue that work in the same language.
Making the specification answer back
A proof about the model leaves an obvious question: does the running application follow it? Our implementation is written in Go and TypeScript. We cannot simply turn the Agda specification into the production code we need.
We can, however, compile it into an executable oracle. Give the oracle an input and it calculates what the specification says should happen. Then we compare that answer with what the implementation actually does.
Property-based testing, in the QuickCheck tradition, lets us generate cases rather than write only examples with predetermined answers. We ask the same question of each: does the implementation agree with the specification? The expected behaviour comes from the compiled model, so we do not translate it by hand into another collection of test expectations.
The implementation remains free to organize its work differently. Its database, internal structures, and choice of algorithms need not resemble the Agda model. What must agree is the behaviour we compare: the result, the refusal, the relevant changes to state.
Each generated case becomes a conformance check. How much confidence those checks earn depends on the cases we generate and the behaviour we observe. They do not prove agreement on every possible execution, but they make the specification an active judge of the implementation.
That gives an AI agent something better than another document to interpret. It can choose an implementation, while an executable version of the rule argues back.
What we give the agent
An implementation task can now refer to a rule with a definition behind it. “Implement cancellation” need not leave the agent to infer what cancellation means from a button label, an existing handler, or its own expectations about subscriptions. The model can say which state changes, which entitlement remains, and when the operation must be refused.
The agent has two ways to consult that meaning. It can read the definitions to understand the intended behaviour, and its implementation can be compared with the compiled oracle on generated cases. The specification supplies both a description to work from and an answer to check against.
A disagreement then gives us a concrete question. Did the implementation depart from the rule, or have we discovered that the rule itself needs to change? The second is a product decision. It should become an explicit change to the model, with the corresponding definitions and proofs reconsidered, rather than disappear inside an implementation patch.
This still leaves room for ordinary language. We need it to explain why we want a change, discuss alternatives, and decide which behaviour is desirable. But the decisions we have settled can acquire a more durable form. The agent can choose how to carry them out without having to silently supply their meaning.
What the word “every” costs
Once the concepts are explicit, we can state laws over them. A refused operation changes nothing. An actor without the required ownership cannot mutate an organization. Deleting an entity preserves unrelated tenants. A revoked or expired grant contributes no entitlement. Every reachable state remains well formed.
These claims range over the entire domain represented by the model. A regression test remembers a particular failure: this input once produced the wrong result. A proof has to establish the law for every admissible state and event covered by its statement. Dressing a few selected examples in formal notation would leave the essential question unanswered.
The word every also changes maintenance. When a transition is defined by cases over a closed event type, adding an event can make that definition incomplete. A preservation proof that proceeds by those cases needs an argument for the new one. The checker refuses the incomplete construction. All the old tests might still pass, but the new operation has acquired an obligation that nobody had to remember to put on a checklist.
That obligation takes work. A change to a datatype can require new arguments far from the original edit. Nor can a checker decide whether we chose a wise policy. It checks what follows from the policy we actually wrote down. The effort is partly the cost of discovering how much we had left unsaid.
A model someone else can recognize
A page of proof machinery can hide the product as thoroughly as a page of machine instructions. Precision would be a peculiar victory if our colleagues could no longer recognize what we were building.
We use SysML to give architects, product designers, and engineers a view of the entities, relationships, states, operations, and lifecycles. Agda supplies the exact definitions and laws beneath that view. The diagrams leave out proof machinery so that the architecture is visible; the formal model settles questions that the diagram alone can leave ambiguous. It is the same bargain we wanted from a programming language: leave out enough to see the idea, without losing the meaning that matters.
This introduces another opportunity for drift, so the relationship is explicit: Agda governs behaviour, and SysML is its architectural reading model. A structural checker catches certain mismatches, such as a state or action missing from one representation. It does not establish that every guard or every line of prose means the same thing in both. Those connections still need review.
The same care applies to production code. A proof about the model does not establish that a SQL transaction or browser screen follows it. Implementation tests exercise handlers, transactions, interfaces, and the seams between them; review and audits examine connections that are not mechanically checked. UI wording and concrete regressions usually belong in requirements and tests. Giving them formal notation would not automatically improve the evidence.
There is no single stamp marked “verified.” We have definitions and proofs, a view people can discuss, checks between selected parts, and tests of the running system. Part of reliability is knowing where each argument runs out.
Leaving something for the next author
An AI agent can now begin with the governing model, instead of inferring policy from whichever handler it opens first. It has a basis for distinguishing an implementation defect from a proposed product change. The compiler and tests can challenge its work independently of how persuasive its explanation sounds.
Keeping this contract takes time. So does reconstructing the product's meaning each time its implementations disagree. I remember what that second kind of work feels like: the printout is in front of me, I can read every line, and I can no longer recover the thought that arranged them.
I would rather keep a home for the intention before it turns into code. Then a future colleague, or an AI agent, can be given more than a plausible sentence. They can be shown the rule, the question behind it, and the answer we chose.
It does not promise perfect software. It may make the thing we are building a little less likely to vanish inside its own implementation.