For more than two thousand years, at least since Aristotle set down his logic, we have known how to prove that something is strictly true. Computer science was born from that same formal root. Turing and his contemporaries built it on a theory of what can be computed and what can be proven, and, just as sharply, of what cannot. And then, in practice, a more pragmatic philosophy prevailed. A compiler today will happily accept a program that is perfectly well-formed and still fails the moment it runs, because we chose to check the form and defer the meaning. That failure is not inevitable. We accept it because checking meaning by hand was never affordable.
That is the strange fact at the center of my recent work. Software is modern, but the thing it could inherit is ancient. Deductive logic, the axiomatic method, the idea that a claim can be established beyond doubt if you are willing to do the work, all of that predates the computer by millennia. The techniques that carry that old rigor into software, types, contracts, tests, specifications, formal methods, are its latest descendants. We have had them, taught them, admired them, and on most real work, under most real deadlines, quietly ignored them.
Not because they are wrong, but because they were too expensive to sustain.
Every one of those disciplines is a bridge. On one bank is what a human means, the intent, the desired functionality, and the constraints, the things we never intended the system to do. On the other is what a machine will execute, exact and literal, where one wrong expression breaks everything. A type signature, a test, a contract, an interface. Each is a small structure that connects the two banks, so the meaning on one side stays pinned to the behavior on the other.
The problem was never the bridge. It was that a human had to walk it, in both directions, forever. Someone had to write the specification, keep it in sync as the code changed, prove the code still matched, and never once skip the step when the deadline loomed. No human team does that indefinitely. So the bridges got built at the start of a project and rotted by month six, into outdated documentation, wrong architecture, obscure names, and decisions no one wrote down.
We have lived this exact inversion before, in mathematics. Whole techniques sat in the literature as sound theory that almost nobody ran, because running them by hand was absurd. They reached an answer by repeating a calculation thousands or millions of times, each step shrinking the error, and a single slip anywhere ruined the result. In 1922 Lewis Fry Richardson spent weeks computing, by hand, a single short weather forecast, using the numerical method behind every forecast today. His own numbers came out wildly wrong. The method was not yet stable and the data was raw, but the approach was sound and, above all, unaffordable by hand. Cheap computation was what eventually rescued it. Monte Carlo simulation, the numerical methods under modern engineering, the transforms under signal processing, the same story in each case, correct for decades and mostly unused. The processor did not make any of that mathematics correct. It collapsed the cost of arithmetic, and a shelf of correct-but-impractical theory turned into everyday work. The same cheap arithmetic later made neural networks practical, and let a 1954 idea of the linguist Zellig Harris, that a word’s meaning is shaped by the words around it, run at the scale where it became the language models we use now.
The disciplines of software correctness have been sitting on that same shelf, for the same reason. And the cost that pinned them there was never only time to execute, it was also learning. Doing them by hand demanded that every engineer hold the full discipline in their head and never tire of applying it. Two costs, time and mastery, and both of them are what made the correct thing the thing you skipped.
Here is what changed.
The transformer, the AI coding assistant, is the first tireless reader and writer fluent on both banks. It was trained on an ocean of human language and a smaller, sharper slice of code. It understands “this endpoint should reject expired tokens” and it can write the code. For the first time the thing that has to walk the bridge, over and over, without getting bored, without cutting the corner at two in the morning, is a machine. It still needs the right directions and constraints, so it does not fall into the water or cross the wrong bridge, but the walking itself no longer costs a human.
But the bridge is not symmetric, and that asymmetry is where the leverage lives.
The model is not weak at writing code. Give it a clear, local task and it produces valid, idiomatic code faster than you can read it. Where it is weak is everything above the syntax. Grasping what the whole system actually needs, holding the vision across a large program, and seeing what already exists. That is not a coding problem, it is a problem of meaning and context, and it is the half where your judgment lives. So the move is to give the model what it cannot infer on its own. Encode your intent in human terms, good names, clear contracts, stated constraints, and make the existing structure legible on the surface, so the model can grasp the whole it cannot hold in its head. You are not so much helping it write code as giving it the understanding that lets it write the right code, and reuse what is there instead of duplicating it.
That is the whole engine.
There is one more piece, and it is about reading, not writing. You do not understand a properly designed and internally documented system by reading every line of its code. You read its structural surface, the interfaces, the tests that act as contracts under TDD, the architectural decision records, the diagrams, the names of classes and methods. That is a small, high-signal slice that tells you what the code does and why. The implementation is derivable from the surface. You rarely descend into it. This is what clean code and part of SOLID were always after, a system you can understand without holding all of it in your head.
An AI session reads the same way, and it has a limit humans do not feel as sharply. As its context grows, it loses focus, and not only when it has to compress. Even a very large window dilutes attention. What sits far back gets less and less weight, by the way the model spreads probability across everything in view, until it is effectively ignored. That is why the models with the largest windows do not make the problem go away. It drops details, and it starts to contradict decisions it made earlier in the same conversation. A reader with a polluted context cannot exercise even a perfect specification.
So the discipline has two halves that mirror each other. You author the specification so a reader with no memory of your intent, a stateless reader, can derive correct output from it alone. And you keep that reader’s context small and high-signal, routed to only the slice it needs, so it can actually derive what the spec makes derivable. The specification is the what. The clean context is the how. Miss either and the bridge collapses.
Does this cost tokens? Yes, plenty, but the number that matters is not tokens spent, it is tokens per correct line. Without authored structure a session burns tokens on code it throws away, on context it re-explains at every cold start, and on drift it repairs later. Authored structure, the harness of specification and automated checks that surrounds the model, moves the spend toward output you keep. Almost any spec-driven method will collapse the time, and the tokens usually cost less than the time they replace. What you do not get for free is a result you can maintain. That is what the structure buys, and it is measurable, which is new. The real question is whether the system holds these properties, the ones that let it survive an audit, pass a process review, and reassure the people who do not write code and do not trust what they cannot see. I name them, and show why they cover the whole lifecycle, in a separate piece.
There is a fair question here about trust. Right now we read the code the machine writes, all of it, because we do not yet trust it, and with good reason. The abstraction layer is still young. But this will not hold, and the reason is old. In the early years no one trusted what a compiler emitted, and careful programmers read the generated assembler by hand to check it. Almost no one does that today. The trust was earned, and inspection narrowed to the few places where a mistake is catastrophic. Generated code is on the same path, with one difference that matters. A compiler earned that trust by being predictable. A model is not, so the trust cannot come from the generator. It has to come from the structure around it, the specification and the harness that verify the output every time. We will stop reading every line, not on faith, but because that structure does the checking. Human review will not vanish. It will concentrate where it belongs, on the critical and the ambiguous, and lift off the rest.
And there is a cost the bill does not show. This is high-load work. Specifying correctly is the hard-won judgment of a serious engineer about what counts as correct for this system, and that is exactly the part that does not regenerate for free. If you were wondering where the human value goes in an age of code-generating machines, that is the answer. And before any of this, there is work the bridge cannot do for you. You have to understand what the user actually needs, and how to build it well with the technology you have. The machine is weakest at exactly that, and cannot yet correct itself. Engineers with real grounding in theory, architecture, and the patterns of complex systems that already work become more essential than ever.
For more than two thousand years the rigor was there, and the cost of using it was the thing we could never quite sustain. That has largely stopped being true. What it leaves in our hands is the older problem underneath, knowing precisely what correct means for this system, which was always the hard-won part of the work anyway.
---
*The white paper, the field guide, and every experiment behind this are open access:* https://doi.org/10.5281/zenodo.21726017 · https://pragmaworks.dev