Long-horizon agents write dead programs
After the OpenAI Navier–Stokes incident, what happened to mathematics finally clicked for me, and it explains something about what has been happening to software engineering.
Have you heard that
- when autonomous agents run long-horizon tasks, you gradually lose your understanding of the codebase: the big picture, the design, etc., unless you are careful to reduce its entropy along the way? Margaret-Anne Storey calls this cognitive debt, “the erosion of shared understanding across a team” (Storey 2026), and Peter Naur argued back in 1985 that this understanding, the theory of the program, is what programming really produces (Naur 1985).
- AI bloats: agents tend to overcomplicate everything and are very defensive in covering every corner case? SlopCodeBench found verbosity rising in 75.5% of agent trajectories, with agent code 2.3 times as verbose as human-written repositories (Orlanski et al. 2026).
- in the last ~18 months, code quality in production has degraded and the number of incidents has increased (Harvey and DeBellis 2025; Orosz and Nilsson 2026)? Charity Majors sees two camps, and “this often starts to come down to the group that is on call and the group that is not.” Those on call “are seeing melting mental models. They’re seeing slop.” (Orosz 2026)
- there’s a wall, beyond which you can ask an agent to add a feature and it will run in circles implementing it? In SlopCodeBench, where agents repeatedly extend their own code as the specification evolves, no agent solves a single problem end-to-end (Orlanski et al. 2026).
The Navier–Stokes incident crystallizes what’s really happening: these super-long-horizon tasks seeking an answer (a verifiable reward) give you something completely logically sound yet indigestible to a human. We’ve lost our understanding of how it arrived at the answer.
In Naur’s terms, it is a dead program. For Naur, a program dies when the team holding its theory is dissolved, and “A dead program may continue to be used for execution in a computer and to produce useful results.” (Naur 1985) With Lean this is literal: a proof is a program, and this one checks. But no one holds its theory. It was born dead.
To some, having an answer is enough—that’s our product. Charity Majors believes it’s a “when” and not an “if” that we ship code we have never looked at, and thus do not understand, to production (Orosz 2026).
But a dead program stays useful only as long as nothing needs to change. Naur’s view explains all four symptoms above with one cause: the output doesn’t have a theory laid out in it.
- Losing the big picture is almost the definition: there is no theory to take in, and every change made without one adds entropy instead of reducing it.
- Bloat: to decide that a corner case can’t happen, or that some code is dead, you need a theory of how the program relates to the world. As Naur puts it, “the decision that a part of the world is relevant can only be made by someone who understands the whole world.” Without it, the safe move under a verifier is to guard everything and delete nothing: a verifiable reward pays for coverage, never for omission.
- Incidents: tests only check what is specified, and what fills the gap between the specification and the world is the theory. That gap is where incidents live, and why those on call are the first to see the mental models melting.
- The wall: modifications made “without a proper grasp of the underlying theory” have “the character of unintegrated patches”, and the death of a program “becomes visible when demands for modifications of the program cannot be intelligently answered.” (Naur 1985) An agent rebuilds its theory from the code in every session. If the code lays out no theory, there’s nothing to rebuild from, and each patch erodes it further.
In vibe coding, and to a lesser extent in agentic engineering, we are trading correctness for speed: say, 10 times the lines of code come out, and correctness goes down. But we kind of have a fix for that: unit tests, specifications, architecture design, linters, static analysis, etc. These give verifiable signals that an agent can pick up and act upon, both in training (reinforcement learning with verifiable rewards, RLVR) and at test time (an agent running in a loop sees an error and fixes it). So correctness goes back up. Not to 100%, since none of these is a formal proof (and were human software engineers ever at 100% anyway?), and the new equilibrium may well sit lower than where we started. But we have a solution. Intercom is one data point: its static-analysis measure of code quality declined as agents wrote more of the code and is now recovering, while downtime from breaking changes dropped by 35% as deployments doubled (Curran 2026).
What we haven’t arrived at yet, demonstrated most clearly in the Navier–Stokes incident, is understanding. Again, we are trading understanding for speed. But here we are a lot further behind: there is no counterpart to the correctness harness. Nothing gives a verifiable signal for whether an output lays out a theory of itself—the right abstraction, a design a human can hold in their head—so there is nothing for RLVR to train on, and nothing for an agent in a loop to act upon. And Naur would say this is not just a missing tool: “the very notion of qualities such as simplicity and good structure can only be understood in terms of the theory of the program.” (Naur 1985) You can’t write a linter for a theory. The only way I know to bake understanding into these long-horizon tasks is to do the understanding part in your specification yourself, and then the speed advantage of autonomous agents is largely erased.
To be clear, I am not talking about how long it takes a human to digest the output. Even a great theory takes time to learn, and that problem existed long before LLMs. If you don’t know what a functor is, Emily Riehl’s resolution of her confusion about direct and inverse images won’t click (see my link post), but learning about functors is a separate concern. The problem here is that the agent’s output doesn’t have a theory laid out in the first place.
Whether a theory can be laid out at all is a fair question. Naur argues the programmer’s knowledge “transcends that which is recorded in the documented products” (Naur 1985). Riehl’s theory building hints at a partial answer: the right abstraction is the part of a theory that does get written down, and it is what makes it easier “for more people to hold increasingly complicated mathematical thoughts in their heads.”
So what do we do in the meantime?
- Keep a human in the loop at intervals, to reduce the entropy along the way rather than after the fact.
- Budget for building the theory afterwards. Someone has to turn the output into something people can understand, as I argued for the 165-page Navier–Stokes proof in What should mathematics reward?.
- Accept that, for now, understanding caps the speed, and decide per project whether that matters. For a product, the answer may be enough. For mathematics, it isn’t: the understanding is the product.
And this is the part I’m still working out. Navier–Stokes is the most extreme example of agentic engineering’s limits: the specification could be made complete, as a Lean theorem, and a machine checked the proof against it. It still wasn’t enough. I’ve argued that research software, at least the kind that establishes scientific results, is closer to mathematics than to product engineering. If so, what should those of us writing simulations and scientific computing code learn from it? I don’t have the answer yet.