[AI goes where the oracle is cheap](/blog/2026/9/1/ai-goes-where-the-oracle-is-cheap)
Paul Dix, writing about [the end of programming](https://pauldix.com/the-end-of-programming):
If you can build a verification system and give proper direction, AI can produce a highly complex, highly sophisticated piece of software and it can continue to refine it until it just works.
His main evidence is the recent rewrite of Bun from Zig to Rust. A common counter is that the agents had an oracle, which explains away the achievement because they were given an existing implementation, a compiler, and an enormous test suite. I think this gets the interesting part backwards, because AI does its best work where it can cheaply discover that it is wrong (machine learning, is that you?). The oracle is not a caveat to the result but what makes the result possible.
Reproducing known behaviour is narrower than deciding what Bun should do, but migrations, compatibility work and implementing behaviour we can already describe make up a lot of valuable programming. Narrow does not mean unimportant when the narrow category is this large.
AI will move fastest through work that is cheap to judge, not necessarily work that is easy to do. We will keep seeing agents pile up impressive results on engineering problems whenever a compiler, reference implementation, proof checker or test suite can tell them when they are wrong. The challenge is much less tidy when the result has to be judged rather than tested. How do you organise a repository, write the specifications and maintain the tens of Markdown files that give an agent enough context to produce something useful? People using coding agents on messy, real work are already finding that implementation gets cheaper while describing the system, its constraints and what good looks like becomes the work.
Formal mathematics makes the same boundary especially clear. A proof checker can reliably reject an invalid proof, giving an AI room to search through many possible solutions to a genuinely hard problem. It can tell us whether a proof follows from the formal statement, but not whether we formalised the right statement or whether the result matters.
Paul calls this the end of programming, which seems like quite a leap. What Bun shows more clearly is that implementation can become dramatically cheaper when correctness is cheap to test, but cheap code does not make judgement cheap. The work is defining what counts as correct, giving agents enough context to act usefully, and then deciding whether the thing you made is actually any good. Taste™.