Total Internal Reflection

Software is hard. Personally, I oppose the position that “writing software was never the hard part”, and believe that that is what people say when they have not explored the space of writing maintainable, extensible software well enough, or have not seen the impact of decisions (both good and bad) that go into building systems that are either maintainable and understandable, or become a tangled, friction-laden maintenance nightmare.

Let me clarify at length what I mean by “writing software”.

What it is not: not merely knowing and wielding the syntax / API of the language / tech stack through and through to get the job done. This is necessary but not sufficient. If that were the case, we would all be writing in assembly language.

What it is: Being able to express domain intention in code, in such a way that said intention is recoverable (ideally mechanically) from the code with minimal context.

We’d like to express our intentions to the computer at a level of abstraction closer to our thought processes. This is what programming languages are for, and, more recently, why LLMs have become a viable step-up in expressing these intentions. But they are also the source of a lot of slop. Slop code is different from plain text slop though: working code is working code, however bad the quality. However, I argue that the degree and fidelity of the encoding of our mental model in software, starts not from the code, but from the specifications that we write, and in the logical extreme, the specification is the code.

For the longest time, we have been writing specifications in plain text, which is a poor medium for encoding a mental model. Ideally, like any programming language, how do we express our intention at a higher abstraction without sacrificing precision?

There are two scenarios where these bear fruit:

Reasoning about existing (possibly legacy) code: This happens mostly during reverse engineering, recovering semantic understanding from existing code. The question then is: what is the best way to model the existing code precisely enough to recover intent and express it unambiguously, without drowning in tech/language-specific details?
Encoding domain reasoning in code that we write: This happens when we are developing new software. The question then is: what is the best way to minimise the delta between our mental model and its expression in code?

Both of these are two sides of the same coin, and both lead to the same question: how do we express our intention at a higher abstraction without sacrificing precision?

We have been doing this with programming languages for the longest time, and the temptation is to treat LLMs as another jump in abstraction. This is not a tenable position, though. The sort of abstractions we have been building programming languages for, do not sacrifice precision. Regardless of the language, the computer does exactly what we tell it to do, no more, no less (sometimes to the chagrin and frustration of the humans writing this code). Plain text, and by extension, LLMs, are inherently a lossy medium, if used to express precise intent for consumption and interpretation by a machine.

The Theses

This is not to dissuade people from using LLMs for programming. The central theses I present in this article are:

Shift the programming model left, from implicit human understanding to explicit deterministic encoding at runtime, and to explicit type- and structure-level encoding of domain reasoning, such that semantic errors and ambiguity are impossible by construction.
Just like good software engineering practices are useful for future (and current) comprehension and reasoning of code to humans and teams, they are as useful to LLM agents for tracing and reasoning through code.
The interesting thing about GenAI is not what it makes newly possible; it is what it makes newly affordable: these are the techniques which enable the two points above; and I don’t see a lot of people spending that windfall on the thing worth buying.

This is an opinionated position, and it is still evolving. I purposefully took a somewhat extreme stance when writing this, because I want to represent something of a mental north star, regardless of the level of feasibility; that depends upon several factors: the language, the tooling, the maturity of the engineering team(s), and so on.

Every technique and tool I am going to describe here predates GenAI by years. Dependent types, TLA+, Dafny, abstract interpretation, Prolog, property-based testing. None of it was ever wrong. It was expensive, needed skill, and slow work that was hard to defend to anyone holding a budget. So most of us stayed on the bottom rung of the ladder and called it pragmatism.

What got cheap in the last three years is exactly the labour that kept us down there. Spending it on generating more unverified code faster wastes the opportunity, and that is what most teams are doing.

AI Proposes; the Verifier Disposes
The Curry-Howard Isomorphism in Ninety Seconds
The Program Is the Proof
The Zoo of Behaviour Verification
Correct by Construction vs. Correct by Observation
Markdown Specifications Are Bullshit
Flavours of Specifications
A Specification You Can Interrogate
Model the Domain, Not Just the Behaviour
Both Ladders End in the Same Place
What AI Actually Changed
The Fundamentals Matter More Now, Not Less
Rigour Theatre
The Harness Is the Trust Boundary
Where This Is Over-Engineering
Conclusion

AI Proposes; the Verifier Disposes

If you want one architectural principle out of this article, it is the heading of this section. Everything after it is the argument for why these four bets and not some other four; if you read nothing else, read this.

As a design-time proposer, a model is welcome absolutely anywhere, as long as the output goes through a deterministic gate before anyone depends on it. Same model, opposite rules, depending on which side of the build it sits.

Here is what it decomposes into.

Executable specs, graded by criticality. The model proposes toward specs that run. Forward: FP discipline first, to get a verifiable substrate at all, then formalism where the language and the stakes both justify it. The verifier disposes by running them: deterministic pass/fail with no human in the gate, and a postcondition violation that localises the fault to one unit rather than to a service.

On inherited code you do not get to choose, and the bottom rung is the only one on offer. Characterisation tests are the way up: they pin existing behaviour as an executable spec, and AI has collapsed the cost of writing them at volume. Two catches, both worth stating. They pin the bugs exactly as written — a characterisation test encodes what the system does, not what it should do, so what you have bought is a regression net, not a specification of intent. And a model writing them has no idea which part of the observed output is behaviour and which is incidental, so it will cheerfully assert on timestamps, map ordering and the exact wording of a log line, and you end up with a suite the team learns to ignore. Above that rung, give the model computed facts rather than guesses: call graphs, def-use chains, reaching conditions, coverage. I have written about the mechanics of this at length in Harnessing LLMs with Deterministic Program Analysis.

Legibility and traceability. Code structured to be read by the next model, not just by the next human. Types encode intent as a machine-readable spec. Traceability is emitted forward, at the point of construction, never reverse-engineered later. The verifier disposes via the type checker, which is a verifier of intent, and via structure that makes reasoning safe without global context.

Functional core, imperative shell. Propose pure functions with no hidden state; quarantine effects at the seam. The verifier disposes because for a pure function the output is the full contract: you can regenerate the implementation freely with no side-effect risk, and safety and liveness properties become model-checkable.

Composable systems, bounded contexts. The unit of comprehension should be a bounded context, not the system, so that no global understanding is required to change anything. The context-window framing is a useful test of whether you have actually drawn the boundary or merely named it: if a context cannot be understood without also loading four of its neighbours, it is not a bounded context, it is a folder. Plenty of contexts in real systems fail that test, and that is a finding about the design rather than about the tooling. The verifier disposes at the contract-checked boundary: a proposal cannot violate a neighbour’s contract without something catching it mechanically.

Every one of those four is an ordinary architectural virtue that predates all of this. What changed is that each one now also determines whether a machine can safely participate in your codebase.

The rest of this article is why. It starts with the reason a verifier is a coherent thing to put at the centre of a development process at all, which turns out to be a theorem from 1934.

The Curry-Howard Isomorphism in Ninety Seconds

The Curry-Howard Isomorphism says that logic and programming are the same structure under two different names.

Logic	Programming
proposition	type
proof	program
A implies B	function `A -> B`
A and B	pair `(A, B)`
A or B	sum `Either A B`
modus ponens	calling the function
checking a proof	type-checking

A claim like “every valid order yields an invoice” is a proposition. Written as a type, it is:

invoice :: ValidOrder -> Invoice

The proof of that proposition is an implementation of that type:

invoice o = ...

If it compiles, the claim holds. Type-checking is proof-checking. Curry found this in 1934, Howard found it again in 1969. It is a theorem, not a nice way of talking about types.

There is one catch, and it matters enormously in the languages most of us actually ship in. Only a total function is a proof. Throw an exception, return null, or loop forever, and you have proved nothing at all. The compiler will be perfectly happy anyway. Most of the industry’s type systems are logics with a hole in them, and everybody has agreed not to look at the hole.

The Program Is the Proof

A proposition is a type. A proof of it is a program of that type. This is exact, not a metaphor. So your running code is already the most exact statement of what your system does. A type, a model, a test, a diagram, a paragraph of English: every one of them is an approximation of that program, and the only reason you buy an approximation is that it is cheaper than the thing it approximates.

That gives you exactly one question to ask about every technique below. How much of the proof does it buy, and what does it cost?

Not “is this rigorous?”, not “is this best practice?”. How much of the proof, at what price.

The Zoo of Behaviour Verification

Here are the ways to be sure your code does what you think, in descending order of certainty and ascending order of regret. The ordering is the point, so for the rest of this article I will call the positions in it rungs, and the whole thing the behaviour ladder.

Technique	What you actually get	Earliest it applies	Cost to adopt
Formal verification: model checking and program verification: TLA+, Dafny, etc.	proves a model, not your code	before any code is written	high: learning the tool, and deciding which properties are worth proving
Correct by construction: rich domain types, dependent types (Lean, Idris), illegal states made unrepresentable	depends upon type system and programmer discipline	write / compile time	moderate: a strong type system, plus modelling discipline
Symbolic execution: abstract interpretation, reaching conditions, taint analysis	works on actual code, depends upon tooling maturity	post-compile	high: specialised setups
Static analysis: lint and immutability, cyclomatic complexity, architectural import constraints	commit and integration gates	build time	low: mostly off the shelf
Static analysis (reverse engineering): control-flow graphs, data-flow analysis, def-use chains, call graphs	recovered, not encoded	any time, on code that already exists	low to moderate, depending on tooling for the language
Pre-production runtime: tests, assertions, ordinary business logic, coverage and assertion quality	instances of the proof, not the proof	build / integration time	low: standard in every language
Production runtime guardrails: monitors, circuit breakers, rate limiters, etc.	instances of the proof, and only after the fact	production	low: standard in most deployment environments
Prose / Markdown: verified by a human in code review, or by production, and by nothing else	nothing here can fail	any time	near zero, and you get what you pay for

One axis does not fit in that table, because it does not track the ordering at all.

How generally applicable is this technique (Narrower -> Wider)?

Production runtime guardrails (cross-functional requirements) -> Static analysis (building blocks) -> Pre-production runtime (both behaviours and CFRs, but specific instances) -> Symbolic execution (behaviours across multiple histories) -> Correct by construction (general program correctness) -> Formal verification (general program correctness, not performance)

There is an asymmetry in that table that I want to talk about.

The ‘Correct by Construction’ rung is forward. You encode the property while you are writing the code, and the compiler checks that you did not contradict yourself.
‘Static Analysis (Reverse Engineering)’ is a somewhat special case, since it is mostly run when comprehending existing code. You are recovering properties from code that somebody else wrote, years ago, without any conscious intention of making them recoverable. That’s reverse engineering. Obviously, a lot of this analysis actually happens inside compilers when they are lowering code, but that is usually transparent to the program writer.
The remaining ones can usually be applied in either direction.
Static analysis and Pre-Production Runtime Guardrails are the cheapest rungs, and there is no excuse whatsoever for skipping them. If your review process consists of senior engineers reading diffs for style and cyclomatic complexity, you are paying six figures for a linter.

Correct by Construction vs. Correct by Observation

Runtime is where most teams find out they were wrong. It is the most expensive place to find out, and the latest. You are not required to work this way. It is a choice, and mostly an unexamined one.

This is what shift-left should mean. Most people use it to mean “test earlier”, which is still runtime, just sooner. Moving your integration suite from Friday to Tuesday does not change the epistemology of what you are doing: you are still observing instances and generalising. The point is to move the correctness argument out of execution altogether.

Markdown Specifications Are Bullshit

I mean specifications written in markdown for machine consumption. Prose for humans is fine and always has been. Prose as the artifact you hand to a code generator and call the source of truth is not.

English is the least exact model of a program you can write. The current fashion is to hand that to a probabilistic system and call the result a methodology. You have stacked two independent sources of ambiguity on top of each other and given the stack a name and a logo.

Here is the operational problem. Nothing in that document can be checked. Not for internal consistency, and not against the code that supposedly implements it. So the checking falls to a human reading a diff, and to production.

“But it’s readable.” Readable by whom, to decide what? A specification nobody can execute cannot fail. People hear that as a feature. A specification that cannot fail, can drift merrily from intent without any alarms.

Prose sits below the bottom rung of the behaviour ladder. A test at least fails.

To be clear about what I am not saying, because it is the obvious objection: requirements arrive in English, and they always will. Prose is fine, and unavoidable, as the input to the encoding step. What it cannot be is the artifact of record, the thing you diff, gate on, and point at when two people disagree. Every technique below is a way of getting the intent out of the English and into something that can fail.

Flavours of Specifications

We still prefer executable specifications, and this can mean several things depending upon the fidelity and effort you want to put into building:

The Code is the Spec

The most faithful executable specification is the program itself. It does not always lend itself to easy reading, but it becomes readable when constraints and rules are expressed readably as part of the code, i.e., a combination of the type system and the behaviours. In the extreme case you can dispense with any other form of documentation: the code IS the spec. If the program’s interfaces are defined by its types, the logic of the program is the proof that these interfaces are satisfied. This is Curry-Howard at its logical extreme. Code that is correct by construction is also cheaper to test, cheaper to change, and cheaper for a machine to reason about. Same property, showing up in three different places on the balance sheet.

Tests

Tests are the current workhorse of the industry: remarkably low-effort to implement, unable to drift silently, a safety net for existing code in the absence of strong type and behaviour guarantees, and a useful design tool if you are practising TDD. They also need to be maintained, they can become unreadable, and, most importantly, they represent instances of the proof of behaviour, not a general proof. You can write tests showing that 2, 4 and 6 are even. That says precisely nothing about 8. This is not a reason to skip tests — most business logic is simple enough that instances will do — it is a reason to be honest about what a green build is evidence of. Tests are the rung you can always afford; that is not an argument for stopping there.

Domain Specific Languages (DSLs)

A lot of domain modelling emerges from prose, and, as stated before, prose cannot be checked. A DSL for business logic is the way out: machine-checkable for consistency, queryable, executable. In the extreme case the code implements the DSL directly, but often the logic is better expressed in a more flexible language. One class of languages I’ve seen particularly suitable for this is Logic Programming: Prolog is the exemplar in this category. I have written about my experiments with extracting out a DSL from a law document in this post.

Static Models

The next level of modelling involves various forms of static analysis: dataflow analysis, which can prove that certain values are never null or that certain functions are never called with certain arguments; dominator analysis, which answers whether this chunk always executes when reaching a certain region of functionality. These are useful for catching bugs, but they are not as powerful as a full proof system. They are building blocks for more abstracted analysis, e.g., answering “which factors affect the interest rate?” might start with dataflow analysis of the interest rate variable.

Static analysis pays the same tax in a different currency. A control-flow graph is precise right up until it hits polymorphism, at which point the call edges point to multiple futures, and further facts must be mined (e.g., dependency wiring configuration) to disambiguate. Every soundness/precision trade-off in an analyser is a place where the model and the code diverge quietly.

Formal Methods

Formal methods — model checking and program verification — are where you model chunks of functionality, assert invariants and properties, and have the tool verify that they hold. This is the space of tools like Dafny, TLA+, etc. They are very powerful, but they require investment in learning them, and more careful thinking about which properties are worth proving (e.g., two users cannot log into the same account).

Different techniques here model different aspects of logic: you’d write a TLA+ spec to verify the safety / liveness of one piece of code, and maybe use Dafny to assert something about a data structure in another. These are not usually used to model the full business domain of a program. TLA+ proves your model has no deadlock. Dafny proves the function you specified is correct. Neither of them has seen your production code. The proof is only ever as good as the model’s resemblance to what you actually shipped, and that resemblance is maintained by hand, by humans, under deadline.

A Specification You Can Interrogate

The rung above guardrails is where it gets interesting, because a declarative spec is a program you can ask questions of. Here is the smallest possible example, written in Prolog.

% the domain, stated once
parent(rajesh, meera).
parent(meera, arun).
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).

:- \+ grandparent(X, X).   % invariant: nobody is their own grandparent

?- grandparent(rajesh, arun).  % forward
   true.

?- grandparent(X, arun).       % backward
   X = rajesh.

?- grandparent(rajesh, Z).     % backward
   Z = arun.

One clause, three questions. You did not write a lookup function and you did not write an inverse lookup function. Resolution ran the rule backwards from the goal, because the rule is a relation, not a procedure.

In markdown you would write “a grandparent is the parent of a parent”, and then check every consequence of that sentence by hand, forever, every time anything else in the document changed.

Note also what the invariant is. It is not a comment. It is not a team convention that gets mentioned in onboarding. Breaking it is a mechanical failure, not a reviewer being alert on a Thursday afternoon.

The limit is worth stating plainly: this does not stop an LLM writing a wrong spec. You can check consistency, not intent. What it does stop is the model being wrong across six paragraphs that nobody reads carefully. And because the check is mechanical, iteration is close to free.

It is also exactly why prose specs cannot be rescued by better models. A wall of text cannot fail, so the loop never closes, so a human has to sit in the middle of it reading everything. You automated the proposing and kept the expensive half.

An experiment on how to extract a deterministic, queryable knowledge base with forward and backward inference from a text document, is documented in A Statute as a Runnable Logic Program.

Model the Domain, Not Just the Behaviour

The grandparent example is trivial on purpose. Put settlement eligibility, tenure calculation, or chain of custody in its place. The mechanism does not change.

The point is that you can ask questions of a domain, deterministically, before a single line of production code exists. Contradictions show up as failed queries. The alternative is two people discovering three sprints later that they meant different things by the same word, which is how most requirements defects actually happen.

Rich typing does the same job, in the language you actually ship. Not “amount is an int, validated somewhere upstream, probably”, but an amount that cannot be constructed outside its valid range. The constructor is the specification.

Domain modelling and type design are the same discipline viewed from two ends. Treat types as annotation and you are wasting the best checker you already have installed and are already paying for.

A worked example of the declarative approach is at github.com/avishek-sen-gupta/doc-pipeline.

Both Ladders End in the Same Place

That is not a coincidence.

flowchart TD
    subgraph CODE[Code ladder]
        R1[runtime tests] --> R2[static analysis]
        R2 --> R3[symbolic execution]
        R3 --> R4[proof without execution]
        R4 --> TOP1[rich domain types]
    end
    subgraph SPEC[Spec ladder]
        S1[prose / markdown] --> S2[deterministic guardrails]
        S2 --> S3[declarative machine-checkable specs]
        S3 --> TOP2[rich domain types]
    end
    TOP1 --> CONV[the type is the proposition\nthe program is the proof\nnothing left to drift]
    TOP2 --> CONV

    classDef default fill:#dde3f5,stroke:#6b7db3,color:#1a1f5e
    classDef bad fill:#fce7f3,stroke:#be185d,color:#831843
    classDef good fill:#d4edda,stroke:#388e3c,color:#1b5e20
    class R1,S1 bad
    class TOP1,TOP2,CONV good

The code ladder climbs to rich domain types: behaviour encoded at compile time, where the illegal program does not typecheck. The spec ladder climbs to rich domain types: the domain encoded at compile time, where the illegal state does not typecheck. At the top, the spec and the program stop being two artifacts that can drift apart. They are one artifact.

This matters specifically for AI-assisted construction. A model’s nondeterminism does not sit everywhere. It sits in the gap between the spec and the program. That gap is the translation step, and translation is where guessing happens. Every rung you climb narrows it. At the limit there is no translation step left for anything to be wrong in.

You will not reach the limit, and I am not suggesting you try. What matters is which way you are walking.

What AI Actually Changed

AI did not add a rung to either ladder. It collapsed the cost of climbing them.

That distinction is the whole argument. Dependent types did not get more expressive because a model can write Lean. TLA+ did not get better at liveness. What changed is that the tedious, skilled, slow labour of encoding things — writing the property, writing the model, writing the characterisation test, writing the query — got an order of magnitude cheaper.

The Fundamentals Matter More Now, Not Less

Immutability. Pure functions. Small composable units. Explicit failure. Contracts at the seams. Types that mean something.

This is not nostalgia. These are the properties that make code checkable, and checkable is what makes generated code safe to keep. Every one of them was a good idea when humans wrote all the code, and we have always given the same reasons: you can read a pure function without holding the rest of the system in your head, you can pass around an immutable value without wondering who else is going to write to it, and you can compose small units without the combination surprising you. What has changed is who else is reading.

Think about what an agent has to do before it can safely change a line of your code. It has to work out what that code does, what it touches, and what breaks elsewhere if it changes. That is the same job you do when you open an unfamiliar file, with one important difference: the agent does it with whatever fits in its context window, and nothing else. It cannot walk over and ask the person who wrote it. It cannot remember the incident in March. Everything it reasons with, it has to recover from the code in front of it. So every property that shrinks the amount of code you must read in order to be sure of something, is worth more to the agent than it ever was to you.

Purity bounds what has to be read at all. For a pure function, the signature plus the body is the entire contract. There is no elsewhere. Nothing in the rest of the codebase can change what it does, which means a model reasoning about it in isolation is reasoning correctly, not optimistically. A method that mutates four fields, reads a clock and writes to a queue has a contract smeared across the whole system, and to reason about it soundly you would have to read the whole system. No context window is big enough for that, and no amount of prompt engineering will substitute for it.

Immutability deletes the aliasing question. Most of the genuinely hard questions in code comprehension are some version of “who else holds a reference to this, and when do they write to it?” Answering it requires global knowledge, which is precisely the thing an agent does not have and a human acquires slowly and expensively. Under immutability the question does not arise, because the answer cannot matter.

Composability makes local reasoning sound rather than merely convenient. If a unit is small, has explicit inputs and outputs, and does not reach outside itself, then understanding the unit is understanding the unit. This is what lets an agent work usefully with a partial view of the system: the view it has is not a fragment of the truth, it is the whole truth about that piece. Bounded contexts are the same principle applied one level up.

Explicit failure removes the control flow the model cannot see. A Result or an Either in the signature is a fact sitting in front of the reader. An exception thrown eleven frames down is not in anything the model is looking at, and it is not in anything you are looking at either during code review. The difference is that you will eventually find out in production; the model will confidently generate a caller that has no idea the path exists.

None of this is a separate discipline you take up for the benefit of machines. It is the same functional programming discipline we have been arguing for since long before any of this, and it pays in all the usual places: pure, immutable, composable code is cheaper to test, cheaper to change, cheaper to verify, and now, cheaper for a machine to contribute to safely. That last one is not a bonus. Increasingly it is the constraint that decides whether a machine can contribute to your codebase at all without degrading it.

Rigour Theatre

Now the objection to everything above, which I think is the strongest one available, and which I would rather state myself than have stated at me.

Making rigour cheap to produce also makes the appearance of rigour cheap to produce. A model will write you a TLA+ spec that model-checks clean, a dependent type that is inhabited, a property test that passes on ten thousand cases — all of which formalise the wrong thing. Consistency is mechanical. Intent is not, and never becomes so. You can check that the spec does not contradict itself; you cannot check that it is the spec you meant.

And rigorous-looking artifacts borrow authority. Nobody re-reads the invariant. It has a \A in it, it went green in CI, and the reviewer who might have caught that it quantifies over the wrong set has already scrolled past. Prose at least advertises that it is unverified. A proof of the wrong proposition is the same failure with better clothes, and the more of it you generate, the less any individual piece gets read.

The second failure is the gate itself. “Deterministic pass/fail with no human in the gate” describes what should happen. What actually happens, when you point an agent at a red build and tell it to make the build green, is that making the build green is the goal it optimises. The assertion gets weakened. The test gets an @Ignore and a plausible comment. The postcondition acquires a special case for exactly the input that was failing. The mock gets adjusted until the thing under test is no longer under test. None of this is malice, and all of it is what “satisfy the verifier” means when the verifier is the only thing being satisfied.

Both of these have the same shape, and the same mitigation. The property, the invariant, the contract, the assertion: these are the artifacts where human judgement is least substitutable, and they are exactly the artifacts you should be least willing to accept unreviewed. Generate the implementation freely. Read the specification like it matters, because it is the only place your intent lives, and keep it in version control where a change to it shows up in a diff rather than in an incident.

So: AI proposes, the verifier disposes, and somebody still has to own the verifier. That is not a hole in the argument. It is where the argument was always going to land, and it is a much better place to be spending expensive human attention than reading diffs for style.

The Harness Is the Trust Boundary

A short detour, because this section is about a different problem from the rest of the article: not building software with AI, but building software that contains it. If you are not shipping an LLM inside the product, skip to the next section.

Not just scaffolding. The trust boundary.

An agent is a component. Components have typed contracts: input schema, output schema, invariants. “But it’s nondeterministic” does not get you out of that; it is an argument for a stricter contract, not the absence of one. A chain of agent calls is a program, and every hop is a function call.

The harness is software you own and test, not glue you paste together. If you have not tested the harness, you have not tested the system, because the agent is not the system.

And record, as they happen, which call, which model version, which prompt, and which gate decision. Reconstructing that afterwards is the genuinely expensive part of debugging an agentic failure, and it is unnecessary.

flowchart TD
    CORE[deterministic core\ntyped, synchronous, owns no AI coupling] --> PORT[port / AI interface\ntyped contract: core knows nothing else]
    PORT --> ADAPT[adapter\ntimeout · retry · circuit breaker\nprompt construction · response parsing · gate]
    ADAPT --> Q[async queue · bulkhead\nnever block the caller · backpressure]
    Q --> API[LLM API\nhigh-latency · partially-failing · nondeterministic]

    classDef default fill:#dde3f5,stroke:#6b7db3,color:#1a1f5e
    classDef good fill:#d4edda,stroke:#388e3c,color:#1b5e20
    classDef bad fill:#fce7f3,stroke:#be185d,color:#831843
    class CORE good
    class API bad

An LLM is a distributed-systems dependency: high-latency, partially-failing, nondeterministic. Treat it as one and the engineering becomes completely ordinary — you already know how to build this. Pretend otherwise and you will meet all three of those properties in production, at the same time, on a Friday.

Where This Is Over-Engineering

Climbing costs real engineering labour, and I am not going to pretend otherwise.

If the thing is low-volume, short-lived and not critical, this is over-engineering and you should not do it. Volume, longevity and criticality are what decide, and they decide per system, not per organisation. Anyone who tells you the ladder is always worth climbing is doing ideology, not engineering.

Rigour also looks slower up front, and sometimes it genuinely is. I am not going to claim it is secretly faster. What I will claim is that a lot of what gets built without it does not survive contact with production, and that cost lands on somebody’s budget anyway — just later, and filed under a different name.

Conclusion

The argument in one line: your program is the proof, everything else you write about it is an approximation you buy because it is cheaper, and the only question worth asking of any technique is how much of the proof it buys and at what price.

That question used to have depressing answers. The techniques at the top of the ladder — dependent types, model checking, declarative domain models, program analysis — were never wrong, they were expensive, and most of us settled at the bottom and called it pragmatism. What changed in the last three years is not the ladder. It is the price of climbing it. The tedious, skilled, slow labour of encoding things is the exact labour that got cheap, and spending that windfall on generating more unverified code faster is the mistake almost everyone is currently making.

So: AI proposes, the verifier disposes. Executable specs rather than prose that cannot fail. Types and structure that carry intent, because the next reader of your code is as likely to be a machine working from a context window as a human working from memory. A functional core with the effects quarantined, because purity is what makes code tractable to a verifier and to an agent alike. Boundaries drawn well enough that a change stays local. None of it is new, and that is rather the point.

What it does not buy you is the judgement about what to encode. Consistency is mechanical; intent never becomes so. The invariant that quantifies over the wrong set will check clean forever, and a gate that nobody owns is a gate that gets optimised around. The expensive human attention does not disappear — it moves, from reading diffs to writing and reading the properties that everything else is checked against, which is a considerably better place for it to be.

So the job of AI here is to make rigour cheap. Not to make judgement optional.