There is a sentence that has stayed with me for more than fifty years, longer than any line of code I ever wrote: don't tell me that it works, tell me how it works. I no longer know exactly who said it to me first, or in what form - it belongs to the air of the discipline I entered in 1969, not to any one paper. But it has quietly organised my whole working life, and it is the right place to start an essay about what AI is doing to software, because AI has made that sentence urgent again in a way it has not been for decades.
Software engineering, as a name, is barely older than I am as a professional. It was coined at the NATO conferences of 1968 and 1969, in the middle of what people were already calling a software crisis: systems too large, too late, too unreliable, built by methods nobody could quite defend. Calling the activity "engineering" was not a description. It was a wager - a bet that programming could acquire what older engineering disciplines already had: theories, predictable failure modes, a body of accumulated knowledge that let you reason about a design before it collapsed on you.
I was there at the beginning of that wager, as a junior participant - which is my excuse for writing this at all.
Through the 1970s and into the 1980s, a serious answer took shape: give programs a mathematical meaning, and reason about that meaning the way a mathematician reasons about a proof.
The foundation came first from Christopher Strachey and Dana Scott, whose joint work gave "the meaning of a program" a rigorous mathematical sense for the first time - Strachey supplying the programming-language side, Scott the domain theory that made higher-order and self-referential constructs tractable. On that foundation, C.A.R. Hoare's 1969 paper gave programmers a way to reason formally about whether a program satisfied its specification - a genuinely different question from whether it ran. Dijkstra pushed the same ambition from another angle, insisting on the distinction between what a routine does for you and how it works, a distinction that is really the same one I opened with.
None of this was abstract mathematics for its own sake. At Oxford, where I later worked alongside Hoare - known to everyone there simply as Tony - he led a team that included Ib Sørensen and Carroll Morgan, and it was this team, with Bernard Sufrin, that tried to bring these methods into contact with a real, large system: IBM's CICS, using the specification language Z. That work fed into the B method - a later, related attempt to derive code from specification - though that is a separate story. It was a serious, sustained attempt to make "engineering" more than a hopeful name.
My own PhD thesis tried to push the same idea one step further: not merely to give a formal specification meaning, but to derive an actual, efficient implementation systematically from that meaning - lexical, then syntactic, then semantic, each level generating its own piece of the eventual program. The underlying question, at every level, was the same: what do we know, what can we derive from what we know, and what remains a legitimate choice left to the implementer?
That question - not any of the names attached to it - is the spine of this essay.
It would be too easy, and wrong, to tell this as a story of failure. Formal methods produced real successes: verified components, systems reasoned about with genuine rigour, a discipline of specification that still underlies safety-critical software today. What they did not do is become the ordinary way software gets built. By 2000, Dijkstra himself, reflecting on three decades of the field, reduced its whole ambition to a single, almost weary sentence: computing's task was "how not to make a mess of it." That is not defeat. It is a mature recognition that complexity had not been tamed, only better understood.
The twenty years after that were not primarily about proof at all. Agile development admitted that requirements change faster than specifications can be finished. Open source turned software into a continuously evolving collective artefact. Cloud and DevOps dissolved the boundary between building software and running it. And underneath all of it, machine learning introduced something the formalists had not planned for: software whose behaviour is not written down as logic at all, but learned from data.
By the time generative AI arrived, the paradigm had shifted from human designs, machine executes to something closer to human expresses an intention, machine produces the artefact. That is the point this essay has been walking toward.
Here is the honest way to put the question. Has AI finally delivered the automation that software engineering was reaching for in 1968 - or has it done the opposite, and separated the production of software even further from the understanding of it?
AI can generate code that compiles, passes its tests, and does what was asked. Fifty years of formal-methods history should make us pause exactly there, because that description - it runs, it works - is precisely the achievement Hoare's 1969 paper warned us not to mistake for a specification being satisfied. A program that runs is not a program whose behaviour has been established against an intention. AI, trained overwhelmingly on code that humans wrote and judged sufficiently useful to keep - not on code whose correctness was formally derived from a specification - may be extraordinarily good at producing the former while telling us almost nothing about the latter.
That is the uncomfortable half of the paradox. The other half is that AI may also be the technology that finally makes the old formal ambition practical at scale - translating loose natural-language intentions into something closer to formal specifications, generating candidate proofs, searching for counterexamples, checking invariants, drawing the links between what a system was meant to do and what it actually does. Understood that way, AI does not obsolete the formal tradition. It may be the missing labour that tradition always lacked the hands to do.
Both things can be true at once, and probably are. The question the essay opened with is not really whether AI can write software - it obviously can, at a volume and speed no team of the kind I trained with could match. The real question is whether our growing power to produce software is growing our power to understand, verify, and control it, or whether those two capacities - so tightly bound together in the founding aspiration of 1968 - are now quietly pulling apart.
If they are, that is not a story about AI replacing programmers. It is the oldest story in this field, told again with a new author: the gap between something that works and something we can say, with evidence, that we understand.
There is a further question waiting behind this one - about what happens when the software an AI produces becomes, in turn, the material it is trained on next, generation after generation, without anyone along that chain having verified the link between specification and implementation even once. That is a different essay. This one ends where it began, with the sentence that has outlasted everything else I learned in fifty years of this trade: don't tell me that it works. Tell me how it works. Software engineering was invented to make that question answerable. Whether AI is finally answering it, or making it harder to ask, is still open.
None of the argument above depends on who taught it to me, but I would be dishonest to leave the debt unnamed. Bernard Sufrin was my mentor at Essex, and I went on to work with him, and with Tony, throughout my years at Oxford. Bernard's gift was both formal and practical - he moved easily in the theory - but what shaped me most was the practical half: an extraordinary capacity to write code that sits close to its specification, in a way I have rarely seen matched since. I inherited his old office at Essex when he left for Oxford; some years later, Tony and Bernard invited me to join them there. I owe a debt too to J. Stoy, whose book taught me denotational semantics before I found myself working near him at the PRG - but it is Bernard's mark that runs deepest through what I have tried to say here.
We love to hear your comments on this article.