The Abstraction Ladder Has Always Been There

There’s a debate happening right now about whether writing formal specifications for AI agents is “real programming” or some kind of ceremonial overhead. The framing is wrong. A spec isn’t an alternative to code — it’s code at a different level of abstraction. And the choice of which level to work at has been the central question of software engineering since 1954.

What abstraction actually is

Every layer of a programming stack is a contract with the same shape: I will state explicitly the things I care about. I will let the layer below decide everything else.

When you write C instead of assembly, you’ve decided you care about control flow and memory layout but not register allocation. The compiler picks registers. When you write Python instead of C, you’ve decided you care about logic but not memory management. The runtime picks allocations. When you write SQL instead of a loop, you’ve decided you care about the shape of the result but not the join algorithm. The query planner picks.

At every step, two things are true simultaneously. You are doing less — fewer decisions, less code, less to get wrong. And you are doing more — more precisely naming the thing you actually want, because the layer below now needs a clear contract to fulfill.

This is the deal abstraction has always offered. It doesn’t remove the work of knowing what you want. It just changes which parts of “what you want” you have to say out loud.

Prompts and specs are rungs on the same ladder

When someone writes a prompt like “build me a payment processor that handles refunds,” they are programming. They’re working at a very high level of abstraction — higher than Python, higher than SQL — where the contract is expressed in English and the layer below (the LLM) fills in essentially everything: language, architecture, data model, error handling, invariants.

When the same person writes a Shen type rule saying balance must be ≥ transaction amount before the transfer is marked verified, they’re also programming. Same ladder. Different rung. This time the contract is expressed in sequent calculus, and the layer below (the LLM plus the type checker plus the compiler) fills in everything except that invariant.

Neither is more or less “real” than the other. Both require the same underlying skill: knowing what you want precisely enough to say it. The English prompt and the formal spec are two points on a continuum that also includes Python, C, and assembly. The only real question is which decisions you want to make explicitly and which you’re willing to delegate.

The decisions you don’t make get made for you

Here’s the part that matters. Every decision you don’t make explicitly, something else makes for you. This is not optional. It is a property of how computation works. Code has to run; the CPU has to do something; some decision gets made at every level whether you named it or not.

When you don’t specify register allocation, the compiler picks — usually well. When you don’t specify an allocation strategy, the runtime picks — usually well. When you don’t specify the invariant that balances can’t go negative, the LLM picks — and here, “well” is doing a lot of work. The LLM will produce code. That code will make an implicit choice about whether negative balances are possible. If you didn’t state the invariant, you delegated the choice, and you won’t know which way it went until something breaks.

The trap in modern AI coding is believing that not writing a spec is the same as not making a decision. It isn’t. It’s delegation to a system with opaque judgment. Sometimes that’s fine — for a throwaway script, delegating everything to the model is exactly right. For a payment processor, it’s catastrophic. The question is never whether to delegate. The question is which things are cheap to delegate and which things you need to nail down yourself.

Why formal specs are just another rung, not a different kind of thing

Formal methods have a reputation for being exotic — a separate discipline practiced by people in academic buildings. The approach this series is about treats them as something much more mundane: another place on the abstraction ladder you were already climbing.

A Shen type rule is a way of saying “here is an invariant I care about; everything else, figure out.” That is structurally identical to writing a Python function signature that says “here is the shape of my input and output; everything else, figure out.” The Python type system is just weaker — it lets more invariants stay implicit. Sequent calculus is stronger — it lets fewer invariants stay implicit. They’re doing the same job with different amounts of precision.

Once you see this, the question “should I write formal specs for my AI coding loop?” stops being philosophical. It becomes the same question you’ve been answering your whole career: which level of abstraction matches the cost of getting this wrong? For a weekend project, prompt-level is fine. For code that moves money, you want a rung where invariants are checked, not hoped for.

This is not new and that’s the point

Every generation of programmers has had a version of this fight. Assembly programmers thought C hid too much. C programmers thought Java hid too much. Java programmers thought Rails hid too much. Rails programmers think prompting hides too much. In every case, the complaint has the same structure: the new layer delegates decisions that the old guard considered essential.

And in every case, both sides were partly right. The new layer genuinely does hide things that sometimes matter. And the new layer genuinely does let you express intent more directly when those things don’t matter. The resolution has always been the same: learn to move up and down the ladder. Pick the rung that matches the stakes. Don’t mistake “I didn’t write it” for “it isn’t there.”

AI coding is the newest rung, and formal specs are a tool for dropping back down a rung when you need to. That’s all. It’s not a paradigm shift. It’s the same abstraction ladder you’ve been on the whole time, with one new step at the top and a useful reminder that the lower steps are still available when you need them.

The rest of this series is about what lives on those lower steps — deductive gates, oracles, defense in depth, and what “knowing what you want” actually looks like when the thing below you can write a thousand lines a minute.