There is perhaps nowhere where AI has made a bigger impact than software engineering. Perhaps the only contender is mathematics. It should be no surprise then that the overlap in these fields is ripe for disruption.
The future of software is going to involve a complete revolution in approach. We now have veritable armies of mid-tier programmers at extremely cheap per-hour cost and this means that LoC (lines-of-code) can be produced at insane scales even in small boutique programming outfits.
Unfortunately the acceptance of code through its review by humans cannot possibly keep up. AI review, while helpful, fails to sort out the core problem of software.
What is the core problem of software?
It is the question “what is this software supposed to do?”. Finding the answer to this problem means navigating users, the market and just plain making good guesses about what sort of behaviour would work well.
Software engineers often say that something is a feature and not a bug, but there is a deep philosophical origin to the question of which is which. The right answer is of course what turns out to be useful.
Specification of what we think the answer should be gives us some sort of record of our current thinking. And it is specification which is going to be central to the new paradigm of software engineering. While in the past open-source developers tinkered with software designs, in the future they will be tinkering instead with specification.
Let me take you on a journey to the future where specification sits at the heart of software development.
But what is a specification
Here I am using a specification to mean a formal description of the intended behaviour. More specifically I’m using it in a very specific way, as a formal description in a theorem prover. This latter part is critical. It means that if we make a claim that some software satisfies the specification, this claim can be certified with a proof - a demonstration that the claim can be checked deterministically by the theorem prover.
Specification could be an elaborate inductive relation but it could also be another program — a program which is clear and readable and shows precisely how we mean for something to take place. As an example, an operational semantics of a programming language is virtually as easy to understand with a simple interpreter as it is with some sort of one-step inductive relation.
But if we are specifying programs with programs, are we then not just running in circles? The answer is: perhaps not. If we say what we mean rather than how we want it done (and often how to do it as fast as possible) it is often easier to make correct and easier to understand.
By way of another example which might make use of inductive definitions, the specification of SQL is very straightforward and compact. We can say precisely what sorts of tables should be returned from an SQL query without talking about how the query takes place or how it is stored on disk. The specification gives huge freedom to the implementation while providing hard constraints on behaviour.
The Concept of the SuperCompiler
When is one programme like another? This question drives so much in theorem proving and optimisation that it could nearly be seen as the central question of software formalisation. That you can replace one programme with another behaviourally equivalent programme is the core idea behind supercompilation.
A compact way of writing that relationship is
p ≃ p'
where ≃ denotes behavioural equivalence.
When I first learned about supercompilation, the idea that one could
take a programme p in a language L and replace it automatically with a
better one, p' in the same language L, I was absolutely fascinated.
The appeal of writing the programme in an idiomatic style and having the “sufficiently clever compiler” transform it into something better was enormous.
Then practitioners showed me things that began to feel like magic. An interpreter, together with its programme and a supercompiler, was itself a compiler for the interpreted language!
Even weirder, you could use a supercompiler as an automated theorem prover. You could write down a program, such as a sort routine, and then write down a program which checked a list for sortedness and the composition could be supercompiled to something which one could check syntactically for truth value. In essence, if correct (and you were a bit lucky), it would boil down to a recursive program whose only branches were True.
Of course this latter approach could not work in the general case or we’d have a decision procedure for specification, which is a violation of Rice’s theorem. Rice’s theorem is sort of the specification world’s equivalent of the halting problem.
And yet it worked for enough problems that the idea of a really powerful supercompiler still appealed. Versions of supercompilation eventually made it into some toolchains, and it was used in some limited ways.
Unfortunately supercompilation suffered from a fatal flaw. The mechanism which made it terminate was also the rule that meant it could not be universally applicable. There can be no single “sufficiently clever compiler”.
One could get a new list of interesting examples, and with a struggle one could write a supercompiler which dealt with them, but there was always one more. This conundrum is sometimes jokingly referred to as the “Full employment theorem”, because there was always one more alteration to be made to the optimiser to absorb some more examples.
Enter AI
With AI, however, the situation changes radically. If you have a supercompiler and you just give the various operations which yield new equivalent programmes to the AI — including importantly the ability to act as an oracular source of potential equivalences which can be mechanically checked, you suddenly get a supercompiler that can close virtually everything. In fact I have not found any examples that it cannot do fairly quickly from the literature and I’ve begun to feed it very hard problems instead. Even complex interpreters with their programmes are no problem for the AI and a relatively small budget of tokens!
We no longer need to fight to find a decision procedure. Instead we can just speculatively try out the AIs on a bunch of transformations and see what happens. This also side-steps Rice’s theorem neatly. We don’t need a termination mechanism and although our border between provability and non-provability is completely unknown, in practice it is able to smash so much of interest in hardly matters. If we think of the immense difficulty of the Navier–Stokes problem — these sorts of prosaic programme transforms are child’s play in comparison. And the AIs will only get better.
I can’t provide you with a proof that it will supercompile your programme because it is impossible. However, if you’ll give me a chance, I can show you that it can. This is the bizarre situation in which AI places us.
The future of AI coding: Specification and Refinement
So what does a software engineering toolchain for human-AI software co-development look like?
My claim is that the next software will be AI-guided certified program refinement. Or perhaps vericoding for short.
It will look like:
- Certifier: A theorem prover
- Language: A language with a formal semantics in that theorem prover
- Specification: A theory of how this formal language establishes specifications
- Refinement: A theory of how one programme looks like another in light of these specifications
Let’s unpack this a bit. We need the theorem prover to establish that our certificates are true. Rocq and Lean are both reasonable candidates for this role.
To use these theorem provers to show properties of software we need to have a formal semantics which can be described inside of the theorem prover. In fact we can use the theorem prover’s own language in Lean or Rocq — this is supported in both environments, but the programme which it “extracts” is not necessarily the most efficient programme. Further we have lots of software already written and completely eliminating it will take a while so we will need toolkits for these languages for some time to come.
Once we have the ability to describe a programme, we need a way to attach it to the specification we have provided. This could be done in many many different ways. We can think of the approach I mentioned before of showing that the composition of a spec checker with the programme yields a normal form. We can have an additional theorem proving framework such as Iris which allows us to establish pre and post conditions on the behaviour of the programme and attach it to “specification state” in some way.
The familiar Hoare-triple form is
{P} e {Q}.
We also need a cheap way of deciding when one programme acts like another - this is called refinement. This turns out to be useful in a range of scenarios. You can use this to optimise a programme by presenting a transformed programme or even an oracularly guessed program that is the same behaviourally. You can show one programme which is simple and meets a specification and then show that a much more efficient program simulates it (again by step-by-step transformation or simply guessing).
We can write the refinement judgement schematically as
Γ ⊢ e ⊑ e',
where Γ records the context in which the refinement is being judged.
The guessing idea might sound a bit crazy but in practice I’ve found that the AIs are extremely good at guessing a faster program. They might need a bit of back and forth to ensure that it simulates the previous but they are willing to spend the tokens.
But then that leads to the final part of the last statement: “in light of these specifications”. What is behaviourally identical is really an equivalence “up-to” some specification. Replacing one programme with another, where one uses more memory locations than the other might be acceptable, or it might not. That needs to be something we can encode in the notion.
In other words, the equivalence itself may be indexed by what we choose to observe:
e ≃Γ e'.
What this means for software
There was an old joke in software engineering that you want software to be cheap, fast, and correct, but you have to choose two. This may no longer be the case at all. We can demonstrate certificates of specification for very high performance programming languages like C or Rust. We can even optimise these programmes and show a certificate of refinement. And all of the proof work, implementation and performance testing can be done by AI meaning it is cheap. The trinity can be one.
The Pudding is the Proof
The proof of the pudding is, as always, in the eating. Does this actually work? I have been doing a host of experiments and the answer is an unequivocal yes.
I have a few proofs in which the programme is fast and arises from extraction, but I’m using the specifications now to show programme transforms and specification on both Rust and C with all proofs closed automatically by AI. Two public examples: parsebot, a certified JSON parser with a proven zero-copy fast path, and SpecAMQP for the AMQP 1.0 specification in Lean.
Of course some say that this doesn’t really solve our AI slop problem, it just kicks the problem up to specification. In some sense they are right — it does move the problem somewhere else, but it also shrinks the size of the problem and the number of problems we have. Far more implementations exist of SQL than specifications of SQL would need to exist. If work goes more into specifying, our surface area of understanding can be radically reduced.
We can look forward to a period of great rationalisation where we talk far more about intent, spend far more time on standards, and implementations can be almost completely automatically constructed and discarded for better ones as AIs fill them with new candidates.
