Long-horizon agents write dead programs

Long-horizon AI agents can now produce logically sound outputs, such as the Lean-verified proof in the OpenAI Navier–Stokes incident, that no human holds a theory for — what Peter Naur in 1985 called a "dead program." The essay argues that while verifiable signals like unit tests, linters, and static analysis can restore correctness, no equivalent harness exists for understanding, and Intercom is one data point: its static-analysis code quality declined as agents wrote more code and is now recovering, while downtime from breaking changes dropped 35% as deployments doubled (Curran 2026). Charity Majors believes it is a "when" and not an "if" that teams ship code they have never looked at to production (Orosz 2026).

After the OpenAI Navier–Stokes incident ../math/navier-stokes-incident.html , what happened to mathematics finally clicked for me, and it explains something about what has been happening to software engineering. Have you heard that 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. 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 ../link/riehl-theory-building.html , 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? 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 ../math/after-math.html research-software-engineering 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.