Software engineering has had two crises before. They had the same shape: something became cheap, and the work moved to whatever was still hard.
We are in the middle of a third crisis.
The working hypothesis of this series, which the essays that follow test rather than assume: Writing code has become cheap. Meaning has not. The gap between them, between what we want and what a machine can check, is where most of the engineering work in the agent era now lives.
Three eras
The history reads cleanly when you draw it.
In the first era (the 1960s and early 1970s), humans wrote code for machines. The machine’s needs were the constraint. We worked in punched cards, assembly, and hardware-specific tricks. Building hardware was expensive; building software, by comparison, was cheap. When a project failed, it was usually because the hardware did not do what we hoped. An anecdote from this era: Dijkstra invented the shortest-path algorithm in 1956 while preparing a demonstration for the ARMAC computer at the Mathematical Centre in Amsterdam. The software was incidental; the hardware was the tricky part. Hardware was the story.
The second era began with what was already called, in 1968, the software crisis, named at the NATO Conference on Software Engineering in Garmisch. Programs had grown complex enough that no one could keep them correct in their heads. Dijkstra would later put it in his Turing lecture: “the competent programmer is fully aware of the strictly limited size of his own skull.” By 1968, on the reading I find most useful rather than a settled history, software engineers had already come to treat the cost of building software as the one that now dominated, where the cost of the hardware it ran on had dominated before. We responded with abstraction and a more declarative style: high-level languages, ways of reasoning rigorously about programs, and design philosophies that made meaning legible to humans first, so that big systems could be kept correct.
The second crisis arrived more quietly, inside that same era, through the 1990s and 2000s. Programs stopped being self-contained. They had to talk to other programs across networks, depend on hundreds of libraries someone else wrote, share state across machines, and survive in environments far more chaotic than the developer’s machine. We built a new set of disciplines for it: distributed-systems thinking, dependency management, DevOps, security as a craft, and the type systems that finally made the surrounding chaos tractable. It never got the “crisis” name that 1968 did, and calling it a second crisis is my framing, not a received one, but the structural shape rhymes: the cost of “it works on my machine” had fallen, and the cost of another thing, correctness in a wild environment, was now what mattered.
The third era, the one we are living in, is different. What is new is not that machines write code: compilers, static analyzers, and code generators have produced machine-targeted code for decades. What is new is that machines now write code for humans: code we are expected to read, review, and maintain, at the same level of abstraction we use during design. And they do everything: define the problem, propose a solution, write the tests, write the documentation. Quickly, fluently, and with no built-in guarantee that any of it is right. The rest of the series argues where an explicit, inspectable guarantee can be earned, against a stated property inside a named boundary, and what mechanisms to put around everything that cannot be guaranteed that way, which turns out to be most of what makes software right.
Where the work moved
When the machine can do all that in seconds, the question is no longer how do we get the code written? The question is: how do we know we got the right thing?
This is the new crisis, and the sentence I keep coming back to is a hypothesis rather than a measurement: the cost of checking software has overtaken the cost of writing it. What would settle it is a number nobody has published, the share of engineering time spent establishing that code is right rather than producing it, before and after agents entered the workflow. What the literature does establish is next door and collected in Harness engineering (forthcoming): on a fixed model, the design of the checking machinery moves outcomes more than the choice of model does. Meanwhile an agent will turn a vague request into a thousand lines of plausible code in a minute, and whether those lines do what we actually meant is a separate problem that someone, usually still us, has to solve.
The cleanest case I know: in 1999, NASA lost the Mars Climate Orbiter on approach. A piece of ground software reported thruster impulse in pound-force-seconds; the navigation software consuming it expected newton-seconds, the unit the interface specification called for. Each program computed correctly. What did not match was the two teams’ shared understanding of the number crossing the boundary between them, and no run of either program could surface a disagreement that lived in what the interface was supposed to mean. The meaning was wrong.
To get serious about that work, we need a distinction. There are two kinds of checking.
Correctness checking asks: did the code do what the specification said? Given a precise statement of what the code is supposed to do, does it actually do it? Tests, types, properties, formal proofs are all ways to answer that question. The community of formal methods has spent fifty years on it. The cost of formal-methods tools was long considered incompatible with most of the software industry’s constraints. There is now early evidence that agents automate work that used to be done by hand: Rango (ICSE 2025) automatically proves 32% of theorems on a benchmark of real Coq projects, and Laurel (OOPSLA 2025) synthesises more than 56% of the helper assertions Dafny needs to discharge real proofs. These are capability results on benchmarks, not a measured drop in the cost of doing formal methods across the industry; what they suggest is that a barrier long treated as fixed has started to move.
Meaning checking asks a much less mechanical question: was the specification the right specification? It is not about algorithms. It is about people, and what they actually want. Whether a specification matches the team’s actual intent depends on what the team meant. Meaning is implicit until someone forces it into words, dynamic as the system meets reality, and ambiguous in its first formulation. A machine can read a specification; it cannot read the negotiation that produced it. This is the territory of product thinking, of building the right software.
Between the two is what I call the meaning-to-specification gap: the work of taking a fuzzy idea of what the team wants and turning it into something a machine can check. Formal methods cover the far end (precise, machine-checkable specifications). Product thinking covers the near end (vague but human-readable goals). Neither covers the middle. And the middle is where most of the engineering work in the agent era actually lives.
That is the territory the series is about. If you take one thing from this post, take this: the work has moved into the gap between meaning and specification, and naming the gap is the first move. The rest of the series argues what to build in it.
What’s next
Why a loop at all asks why the answer to this crisis has to be a loop rather than a better prompt, a better model, or a better review, and gets there from a one-line model of what an agent is.
After it come the loop I run, the engineer at its centre, and one essay for each discipline the loop rests on. The map of the whole series, with what each essay is for, is at the foot of this page.