The Expensive Fictions of Low-Level Programming Languages
Structure and Guarantees
SubscribeSign in
The Expensive Fictions of Low-Level Programming Languages<br>AI coding tools are facing a major handicap in using popular languages.
Adam Chlipala<br>Jun 30, 2026
Share
I’ve been telling parts of the story of a future with trustworthy search processes that automate software development. If we have a clear and specific-enough formal specification to start out with, then recursive self-improvement can proceed in a way guaranteed to align with our goals. I talked through a number of reasons for optimism on that front, including lessons from recent use of formal verification (for connecting verified pieces together and anticipating new security threats) and speculating about changes in an economy dominated by AI agents (simplifying user interfaces and requirements gathering). The first point of informed skepticism about this idea is usually about the challenge of writing such specifications. There are still plenty of challenges left in assembling good specifications for highly capable systems, but let me now turn to further challenges, which apply after specifications are written.<br>Let’s consider in general the problem of automatic generation of code from its specification. Many AI coding assistants are being used today to write code in a “best effort” way, where the result may include mistakes such that the generated program does not follow its specification. I’m most interested (and future posts will most commonly discuss) methods that are correct by construction, where a tool might give up but will never return an incorrect program. An especially interesting approach is structured search through the space of programs, using formal verification as a fitness function to evaluate intermediate and final program variants.<br>Thanks for reading Structure and Guarantees! Subscribe for free to receive new posts and support my work.
Subscribe
Regardless of what approach is taken to automatic programming, we face conflicting desires to, on the one hand, simplify the space of programs and how we reason about it automatically; and, on the other hand, generate the highest-quality programs in the end. The rub is that higher-quality programs may be longer and more complicated than their lower-quality cousins, requiring more expensive search to find. An important determinant of the effectiveness of search is choice of programming language(s). My main claim in this post is that widely used programming languages are poorly suited for this style of search, especially when we are trying to write high-performance programs – which will be the case when we think about a program-search system recursively improving itself, given how much time and space a complex search can take. To argue this claim, I will start by spelling out a general framework for program search, and then I’ll draw attention to a missing ecological niche within that framework that is underserved by widely used programming languages.<br>Searching the Space of Programs
Let me describe at a very high level a process of gradually refining a specification into a final program. Arguably, human software engineers work in this way, and we can expect to rely increasingly on programs that automate the process. There is a tradition in computer science that makes the ideas formal, called derivation by stepwise refinement, but I’ll leave things largely informal here. We can think of the exploration as moving from the top of the following schematic depiction to the bottom.
The highest levels of the diagram deal with relatively abstract notation and therefore allow the most functionality to be covered by the shortest descriptions. The lowest levels are closer to the computer hardware we plan to run on, and they require details to be spelled out in excruciating detail.<br>Every node of this search is a program in some programming language. Every language we choose should pay off in tractability of search, control over details of the final program, or both. The most straightforward model is that we start off choosing languages biased toward simplifying search and eventually transition to languages that provide low-level control, though mixing the benefits throughout is also fine. Regardless, it should be a red flag if we are ever working with a language that scores poorly on both axes… yet I will claim that today, AI code generation is overwhelmingly working with such languages.<br>Low-Level Programming Languages
Let’s think in particular about languages suitable for the lower levels of the search process. A very dedicated software engineer might work directly with assembly language, almost the lowest-level form of programming undertaken today. However, it would be much more common to bottom out at a programming language like C, which was invented in the 1970s and has overwhelmingly influenced the design of low-level languages. More precisely, such languages are meant to allow...