Code agents made producing software cheap. They did not make understanding what to build, checking that it is right, or remaining accountable for it cheap. That is where the engineering work has moved.
This blog studies that move from an unusual intersection: formal methods, programming-language research, and responsibility for production engineering. The essays derive claims from explicit premises, attach them to inspectable artefacts where possible, and remain open to revision when evidence or a good objection demands it.
The corpus is still growing. These three paths use only published essays; none will send you to a promise disguised as a link.
I build software
Start with Why a loop at all?. It gives a minimal model of an agent and derives the engineering consequence: the durable object is the generate–check–decide loop around it, not the code it emits.
Then read The Code Agent Crisis for the larger historical argument: every software crisis begins when one part of the work becomes cheap and exposes what remains hard.
Take this question back to your next agent session:
When the output is wrong, what should change in the system so that the same class of error becomes harder to produce again?
I lead engineers
Start with The Code Agent Crisis. Its useful claim for an engineering organisation is not that agents write faster. It is that the cost centre moves from production toward meaning and validation.
Continue with Why a loop at all? to see why model choice and prompting are only parts of the system a team must own. The surrounding context, checks, routing decisions, and human judgment are engineering assets too.
Take this question to your team:
Which failures are we repeatedly repairing by hand instead of turning into knowledge, specifications, or checks?
I work on languages, verification, or research
Start with The Code Agent Crisis for the boundary the series draws between correctness and meaning. A proof can establish that a program satisfies a specification; it cannot establish that the specification captures what people need.
Then read Why a loop at all? for the generate–check–decide model and its argument about imperfect verifiers. This is where formal machinery meets an intent that remains human, sociological, and revisable.
If you want the older technical foundations, the About page points to selected work in proof engineering, parsing, programming languages, and computer-science education.
Take this question back to your own work:
Where does your method begin—and who owns the work required before its first formal statement can be written?
The thesis in one paragraph
Fundamental software engineering matters more under agents, not less. Teams need to engineer four things together: the software’s structure, the knowledge available to the agent, the harness that produces and checks changes, and the engineer’s own ability to understand and steer the evolving system. The bridge from ambiguous intent to checkable specification is the common problem. The essays ahead develop those disciplines one by one.
These are living essays. Material revisions are recorded on the Changes page, and new publications appear in the RSS feed.