I wrote recently about the imminence of regular regeneration of large code bases, where software code as we know it should become a throwaway artifact, regularly recreated from evolved requirements by powerful automation. After a quasi-digression on one mechanism to kick off widespread generation of better versions of important programs, I want to return to addressing comments on the earlier article (on LinkedIn, GeekNews, LessWrong, and ACX). I’m writing this blog precisely to get that kind of feedback, to spot holes I unintentionally left in explanations, so I can correct them for the book I plan to write based on this material. So, many thanks to the commenters who spotted those holes and spoke up! I’m going to use the example of database query language SQL to explain more directly the approach I’m arguing for.
Just Another Increase in Programming Abstraction (Kind Of?)
Some of the points I made are unusual enough that they deserve repeating, since much of the feedback assumed I was suggesting a flow closer to conventional approaches than I intended. Let me give a highest-level recap that sets up that discussion productively. I made two claims, one that is absolutely orthodox in Silicon Valley today and one that represents an edgy departure. The orthodox claim is that powerful automation of software development allows us to think of software code as no longer expensive to produce, to the point where we can routinely throw away all of our code and regenerate it, following improved requirements for what it should do and how it should work. Almost all of the excitement around that direction leans heavily on LLMs and assumes that we generate software from natural language (which includes formats like EARS that add modest structure on top of natural language but still require natural-language processing to interpret). My edgy claim is that we need to ditch natural language entirely, for periodic regeneration of large code bases to be practical. Unambiguous specification languages are going to be a crucial ingredient well-known from formal verification but not deployed nearly as widely as LLM-based tools (despite decades of head start for formal methods!). (There is some subtlety to that last point where we want to retain some benefits of LLMs to help understand informal requirements, which I’ll return to later in this article.)
Some of the comments argued that a good unambiguous specification language becomes “just another programming language,” making the argument here overblown. Indeed, I used exactly that historical framing in the original article! I used the example of how the software-development process used to include drawing flowcharts, relatively informal diagrams that were not processed by computers. Then human programmers (separate from the analysts who drew the flowcharts) translated them into assembly language. Eventually, however, automatic compilers were developed, to translate from new high-level programming languages like FORTRAN. A program “planning” format was much more pleasant when further implementation could be automated.
I wrote that a move to writing “specifications” instead was a natural progression in that direction. We had just been stuck waiting for the right technology to automate implementation from there! Still, what exactly makes a specification different from a program? They sit on a spectrum, and sometimes it makes sense to use the same languages to write both.
However, I’ll argue that “specification” usually implies two important characteristics that are unusual in “programming.”
A specification is written to explain what functionality is desired, not how to accomplish it. The most concrete and familiar example is performance, like how quickly a program runs. Much of the complexity of code in practice comes from cleverness in data structures and algorithms to improve performance. I would argue that a great specification should spell out requirements on performance (and indeed a variety of projects have shown how to prove performance requirements of real code, as in one of my own recent papers) but not get into detail on how to meet the requirements. In many cases, specifications can be much simpler and easier to audit precisely because they don’t precommit to optimization details.
A specification often includes nondeterminism to provide flexibility to implementers. We can again find some of the clearest examples in connection to performance. Think of some process that generates a set of answers, and the user is happy to receive them in any order. Depending on how the underlying data were stored, some order may be the most natural, as in reading off the cells of a data structure in the same order as they appear internally. It would be bad for a specification to mandate a particular order, because then it becomes harder to take advantage of a clever new data structure that changes internal order.
A great example to illustrate both points is SQL, the popular database query language. It is possible to write an SQL query that is close to the most compact, straightforward way to describe what constitutes a correct answer. (Cue here complaining by programmers about the concrete syntax of SQL, yeah, yeah!) SQL also gives database engines freedom to return answers in convenient orders, when order isn’t explicitly mandated in a query. Unfortunately, SQL queries do not typically include explicit performance requirements, which could help database engines make tradeoffs intelligently, but I hope future systems get there.
Now, SQL is also a great example of how “specifications” and “programs” live on a spectrum. SQL power users often spend inordinate amounts of time tweaking queries to improve performance. One canonical example is declaring a new index to the database engine, a suggestion of a data structure that may be useful to speed up queries. The hardcore version involves deep inspection of query plans to find bottlenecks in the code that the database came up with. Nonetheless, “pristine,” high-level queries remain highly effective as specifications: easy to read, leaving much flexibility to explore different implementation strategies. It would not be entirely misleading to restate the central point of my last article as more of programming should become more like SQL (including the possibility to start with relatively abstract code, often get satisfactory implementations from it with full automation, and sometimes invest in more-manual improvement that involves adding details to the specification within the same language).
Note how the last little example is a template for how to handle improvement of specifications in other dimensions beyond performance. Through either predeployment testing (of the specification or generated implementation) or observing faults in the field, we can notice and fix specification problems. Examples of other dimensions particularly easy to misspecify are security, privacy, ease of maintenance (DevOps-style), and human usability. Just as with conventional software development, we should expect to keep improving code concerning these aspects – just trying to keep it succinct and put it in specification instead of implementation.
It turns out this style of thinking has a long history in basic research. To start with, we have the relatively informal (or at least typically disconnected from rigorous proof in practice) discipline of requirements engineering. More relevantly, the idea of refinement of specifications into implementations has been studied since at least the 1970s (see a paper by Niklaus Wirth, inventor of the Pascal language). I’ve been working in that tradition myself, including in the Fiat project, where we even used SQL-style notation as a central example for automated refinement with proof.
Relatively declarative configuration languages, say for cloud platforms, are another example that came up in discussion. Amazon’s Zelkova was an early success for formal methods in this area. I think of such tooling as important, but it also seems to solve a fundamentally simpler problem than general software development, and it’s the latter I want to focus on.
The Software Lifecycle with Strong Automation
I hope this framing already suggests some of the details of a future workflow based on unambiguous specifications, because it will look a lot like programming with SQL looks today. Database engines produce query plans automatically from SQL queries. As a result, we save the SQL queries in version control systems like Git, the canonical way of recording code over time, but we don’t put the query plans in version control. If we need to give the query planner instructions, say by requesting indexes, those instructions do go in version control. The point is that what persists, what is not a throwaway byproduct of automation, is exactly the information that makes remaining code generation sufficiently predictable, allowing it to meet our requirements reliably.
One important point I’d like to make here is that remaining stages of code generation don’t need to be deterministic. If requirements were spelled out precisely enough, we can be happy to receive any final, running system that meets the requirements. It’s OK if we get a different one each time! Programmers are used to mandating more determinism than strictly required by their development and maintenance processes, because they aren’t used to writing sufficiently constraining specifications/programs. The earlier SQL example is a good one: because we don’t trust the database engine to choose the right data structures and algorithms, we worry about changes to the subsystem that plans query execution, but what if we annotated our queries and indeed our whole programs with performance requirements instead? Then nondeterminism becomes desirable because sometimes the programming tools find new and better, faster implementations and drop them in without needing to bother us!
The underlying issue is that programmers worry (justifiably) that some important characteristics of the final system can’t be predicted from the source code alone. Yet, because those characteristics are important, we need to make sure we confirm they are suitable. The most common tool is testing, subjecting the generated code to many scenarios and checking it behaved properly. Over time, developers build confidence in even the parts of generated systems that those developers didn’t write themselves, by running many tests over many versions of the program. If a clever programming tool completely changes up those aspects, we have to restart the confidence-building exercise.
I want to emphasize the two big changes to this flow that I’m recommending. The first is to write specifications so precise that literally any realization of them is acceptable. The thought experiment is for, say, a company building a product to imagine that its biggest competitor gets to write any program that meets the specification. The second important change is to rely on machine-checked mathematical proof that a generated program meets its specification. Now we need not rely on testing to find internal bugs in the generated code, as testing covers only particular execution scenarios, while a proof covers all of them. The risks that remain are in the specification, perhaps most importantly in how we characterize the other systems that ours interacts with – so testing should be focused on that interface boundary, and it can be done against a specification that happens to be executable, not the generated implementation. We no longer need to treat e.g. a tricky concurrent data structure that is purely internal as highly suspicious from a bugs standpoint. This shift is similar to the one that happened with programmers trusting the implementations of higher-level programming languages (though there’s no need for trust, as compilers are a great subject for formal verification).
Another concern came up for having tools choose data structures automatically. How does a program evolve over time if the data format keeps changing, leaving prior databases obsolete? This problem is actually addressed pretty naturally: part of the specification for the next version of a program is that it is able to begin with the old contents of a database, where now the specific format of that database is part of the specification of the new version. The code-generation tool may now either keep the database format the same or generate a migration to upgrade to a new representation. (Note that this concern helps us notice a wrinkle of needing to save generated data schemas in version control or similar, even if they were produced automatically.)
Feasibility of Specification and Verification
Some concerns were expressed about scalability of such methods to very large code bases. It’s important to keep in mind which measurements of size we should worry about. It would be strange for a conventional project to measure code size by the amount of machine code generated by compilers. Instead we measure source code, which is checked into version control. Similarly, raising the level of abstraction, we should be worried about the size and maintenance complexity of specifications. Different programs may have vastly different size gaps between specifications and machine-executable code. We’ll have to see how the specifics turn out, but one orienting principle I’m comfortable asserting now is that such a gap often corresponds to the sophistication of performance optimizations in a program (which shouldn’t also be in the specification), so the gap is likely to be widest in domains with lots of attention to performance.
Some readers were skeptical that the LLM-style experience of getting a pile of complex code written on command can ever dovetail with high confidence in correctness – and I actually agree! I’ve argued that deep learning is better understood as a generalization of search engines than as a “reasoning engine” in the colloquial sense. Coding agents are doing something very similar to copying and pasting from existing code bases into a new one, losing the lineage of vetted good ideas. Instead, I’ve already argued for combining reuse of flexible components with AI code generation, where that generation now just needs to reference components by name. The novelty density of all software worldwide is much lower than the novelty density encountered examining all the parts of a single system, and we should be taking advantage of that low novelty to share carefully vetted code across projects. It should dramatically decrease the program-specific reasoning and proof that needs to be carried out. The effort to build, specify, and verify the components scales well with their potential many uses.
Another dimension of skepticism was the effectiveness of formal-verification tools in checking whatever code has been produced. There is a definite tradeoff between accepting a buggy program or failing to validate a correct program (see our past discussion on undecidable program analysis). In cases where the stakes are low enough, it may make sense to adopt a flow that occasionally lets a bad program through, if it enables more development velocity and creativity by coding agents. However, I personally most favor methods that don’t separate code generation from verification. Correct-by-construction techniques interleave correctness reasoning with all steps of writing code, and I’ll have much more to say about this approach in upcoming articles.
Coming up with a sufficiently constraining specification can be hard and error-prone work. Familiar quality-assurance activities for software may switch to specifications instead, including running specifications against many test cases. Tools for simulation, debugging, code review, and so on can also be very helpful for specifications – and all the above practices are actually already common among users of formal-methods tools like proof assistants. However, I would say most engineers not familiar with formal methods are much too pessimistic about the paths toward high-quality specifications. The reason is that most specifications apply to components that ought to be internal to larger systems, and end-to-end verification of full systems catches specification mistakes in internal components very reliably. For instance, a programming-language implementation is tough to specify in isolation, as we need to legislate exactly what each language feature means, but when that language is used internally in the proof of a larger system, we force ourselves to catch any language-design mistakes that are consequential, falsifying what we hope is a simpler top-level specification of an application, and the language definition becomes untrusted (in the good sense of not being assumed correct). There’s also a handy bonus for catching certain security bugs by proving almost any interesting specification about a system.
We can also keep benefiting from LLMs and similar future tools. Coding assistants can be used to write specifications that are then code-reviewed, tested, and so on, at the level of unambiguous specifications. There is an established research area around programming by example, and such techniques could be used to help write specifications automatically from input-output examples or even, with AI assistance, “user stories” that spell out in English ways that programs should be able to be used. The point is that AI can make mistakes, but the final quality assurance is done against an unambiguous specification (which persists in version control, while natural-language dialogues may not).
Aspects of the pushback about nondeterminism of code generators do indeed sound like trouble to me. I wrote previously about how nondeterministic specifications can promote security vulnerabilities through so-called side channels. It also isn’t hard to see how getting the same answer every time can be helpful, for instance in reproducing data analysis from scientific experiments. In such cases, we can make sure that top-level specifications are deterministic, though it may remain useful to allow systems to be built out of components with specification nondeterminism that is hidden well at the system level. A great example is a low-level memory allocator that assigns memory addresses to different pieces of data, where higher-level code is written carefully not to reveal which addresses were assigned. It pays off to allow new versions of the allocator to introduce clever new algorithms that affect address choices.
There was also a question about whether specifications are just pseudocode, and I think they probably aren’t. That terminology usually implies some use of natural language to explain important behavior, which isn’t compatible with truly reliable automatic programming.
Remaining Questions
One interesting question I received was about the place of undocumented features in software that is regularly regenerated. That is, conventional software ships with incidental features that the developers may never have meant to promise to retain indefinitely, and yet users come to depend on them (as laid out in Hyrum’s law). If regeneration can change such incidental features arbitrarily, users may repeatedly be disappointed. For now, I think my strongest response is that undocumented features are bad, and automation may be able to help us avoid them! However, it’s worth thinking about the consequences of users increasingly becoming AI agents themselves. One of my earlier articles analyzed how the problem of ensuring happy users becomes easier then, for instance because new releases can be checked against the code of known users, to make sure they remain satisfied in all possible scenarios. Achieving a similar benefit for human users remains an interesting software-engineering research question.
Complicated systems must often be debugged in the field, as much as we may hope broad formal verification catches all defects. Some bad behaviors only emerge at scale in real environments, which may include components not yet specified or verified. Generated code can still be provided with, for instance, mappings of running code to the parts of specifications that determined it, along with whatever other annotations best support debugging by humans or machines. Indeed, the quality of debugging collateral could be mentioned explicitly in a specification! However, the details definitely constitute an independent research challenge.
Another interesting comment was about how the world and the connections between its pieces seem on an unstoppable upward trajectory of complexity. Methods based on code generation from unambiguous specifications may hit an applicability wall, past some world-complexity threshold. It’s interesting to speculate about how increased adoption of AI may change this phenomenon. On the one hand, “smarter” AIs may go even further in designing complex, society-scale systems. On the other hand, the selection pressure to enable efficient reasoning by AIs may motivate them and us to create bubbles of improved legibility within which economic systems and reasoning systems are codesigned. The world may seem to grow increasingly complex and illegible to humans while AIs are actually improving their ability to keep up!
We all see how amazingly effective LLM-based coding assistants have become, even if it can be hard to build confidence that they wrote the programs we really want. There is an even older tradition of research in program synthesis. I think there’s a lot of exciting technical work to do to draw on these starting points and create the most effective systems for automatic programming. However, it was an intentional omission not to go into more detail in the prior article, as I’m going to need multiple articles worth of content to do that subject justice; stay tuned. For now, just imagine that some reasonable notion of mathematical program proof is fixed, with ideally one standardized trustworthy checker, opening the door to a variety of methods that produce proofs (in the style of proof-carrying code).
I do want to tease now that I see performance of logic-based automated-reasoning tools as a major bottleneck holding back the area. At a minimum, we need these tools to keep up with deep learning-based tools that may be writing code creatively. A major theme of future articles will be full-stack performance engineering to improve logical reasoning and code generation. In fact, I hold out hope that logic-based alternatives will be able to run even faster than purely LLM-based methods, even if LLMs are baked into custom hardware, because of the inherent performance bottlenecks of deep learning.
Next, though, I want to turn to perhaps the hardest case of complete-enough specification being discussed today: AI alignment, the study of how to build flexible automated decision-makers that we should believe will respect our values and not harm us in surprising ways. My impression is that the conversation so far leans very much on thought experiments not connected to implementations, somewhat justifiably if we may (?) not yet have AI powerful enough to exercise the alignment challenge very thoroughly. I’m going to analyze the problem from more of an engineering perspective, grounded in experience building and maintaining significant proofs of system correctness. The gimmick will be thinking of human brains as a legacy system that is worth engineering around if we can, especially if it must be mentioned in the top-level interface of a system.
This post is crossposted from my Substack, Structure and Guarantees, where I explore how formal verification and related ideas might scale to more complex intelligent systems. I argued here previously for a certain approach to regularly throwing away and regenerating program code, without requiring human checking of the results. The comments helpfully pointed out important details that I glossed over, and this post clarifies them.
I wrote recently about the imminence of regular regeneration of large code bases, where software code as we know it should become a throwaway artifact, regularly recreated from evolved requirements by powerful automation. After a quasi-digression on one mechanism to kick off widespread generation of better versions of important programs, I want to return to addressing comments on the earlier article (on LinkedIn, GeekNews, LessWrong, and ACX). I’m writing this blog precisely to get that kind of feedback, to spot holes I unintentionally left in explanations, so I can correct them for the book I plan to write based on this material. So, many thanks to the commenters who spotted those holes and spoke up! I’m going to use the example of database query language SQL to explain more directly the approach I’m arguing for.
Just Another Increase in Programming Abstraction (Kind Of?)
Some of the points I made are unusual enough that they deserve repeating, since much of the feedback assumed I was suggesting a flow closer to conventional approaches than I intended. Let me give a highest-level recap that sets up that discussion productively. I made two claims, one that is absolutely orthodox in Silicon Valley today and one that represents an edgy departure. The orthodox claim is that powerful automation of software development allows us to think of software code as no longer expensive to produce, to the point where we can routinely throw away all of our code and regenerate it, following improved requirements for what it should do and how it should work. Almost all of the excitement around that direction leans heavily on LLMs and assumes that we generate software from natural language (which includes formats like EARS that add modest structure on top of natural language but still require natural-language processing to interpret). My edgy claim is that we need to ditch natural language entirely, for periodic regeneration of large code bases to be practical. Unambiguous specification languages are going to be a crucial ingredient well-known from formal verification but not deployed nearly as widely as LLM-based tools (despite decades of head start for formal methods!). (There is some subtlety to that last point where we want to retain some benefits of LLMs to help understand informal requirements, which I’ll return to later in this article.)
Some of the comments argued that a good unambiguous specification language becomes “just another programming language,” making the argument here overblown. Indeed, I used exactly that historical framing in the original article! I used the example of how the software-development process used to include drawing flowcharts, relatively informal diagrams that were not processed by computers. Then human programmers (separate from the analysts who drew the flowcharts) translated them into assembly language. Eventually, however, automatic compilers were developed, to translate from new high-level programming languages like FORTRAN. A program “planning” format was much more pleasant when further implementation could be automated.
I wrote that a move to writing “specifications” instead was a natural progression in that direction. We had just been stuck waiting for the right technology to automate implementation from there! Still, what exactly makes a specification different from a program? They sit on a spectrum, and sometimes it makes sense to use the same languages to write both.
However, I’ll argue that “specification” usually implies two important characteristics that are unusual in “programming.”
A great example to illustrate both points is SQL, the popular database query language. It is possible to write an SQL query that is close to the most compact, straightforward way to describe what constitutes a correct answer. (Cue here complaining by programmers about the concrete syntax of SQL, yeah, yeah!) SQL also gives database engines freedom to return answers in convenient orders, when order isn’t explicitly mandated in a query. Unfortunately, SQL queries do not typically include explicit performance requirements, which could help database engines make tradeoffs intelligently, but I hope future systems get there.
Now, SQL is also a great example of how “specifications” and “programs” live on a spectrum. SQL power users often spend inordinate amounts of time tweaking queries to improve performance. One canonical example is declaring a new index to the database engine, a suggestion of a data structure that may be useful to speed up queries. The hardcore version involves deep inspection of query plans to find bottlenecks in the code that the database came up with. Nonetheless, “pristine,” high-level queries remain highly effective as specifications: easy to read, leaving much flexibility to explore different implementation strategies. It would not be entirely misleading to restate the central point of my last article as more of programming should become more like SQL (including the possibility to start with relatively abstract code, often get satisfactory implementations from it with full automation, and sometimes invest in more-manual improvement that involves adding details to the specification within the same language).
Note how the last little example is a template for how to handle improvement of specifications in other dimensions beyond performance. Through either predeployment testing (of the specification or generated implementation) or observing faults in the field, we can notice and fix specification problems. Examples of other dimensions particularly easy to misspecify are security, privacy, ease of maintenance (DevOps-style), and human usability. Just as with conventional software development, we should expect to keep improving code concerning these aspects – just trying to keep it succinct and put it in specification instead of implementation.
It turns out this style of thinking has a long history in basic research. To start with, we have the relatively informal (or at least typically disconnected from rigorous proof in practice) discipline of requirements engineering. More relevantly, the idea of refinement of specifications into implementations has been studied since at least the 1970s (see a paper by Niklaus Wirth, inventor of the Pascal language). I’ve been working in that tradition myself, including in the Fiat project, where we even used SQL-style notation as a central example for automated refinement with proof.
Relatively declarative configuration languages, say for cloud platforms, are another example that came up in discussion. Amazon’s Zelkova was an early success for formal methods in this area. I think of such tooling as important, but it also seems to solve a fundamentally simpler problem than general software development, and it’s the latter I want to focus on.
The Software Lifecycle with Strong Automation
I hope this framing already suggests some of the details of a future workflow based on unambiguous specifications, because it will look a lot like programming with SQL looks today. Database engines produce query plans automatically from SQL queries. As a result, we save the SQL queries in version control systems like Git, the canonical way of recording code over time, but we don’t put the query plans in version control. If we need to give the query planner instructions, say by requesting indexes, those instructions do go in version control. The point is that what persists, what is not a throwaway byproduct of automation, is exactly the information that makes remaining code generation sufficiently predictable, allowing it to meet our requirements reliably.
One important point I’d like to make here is that remaining stages of code generation don’t need to be deterministic. If requirements were spelled out precisely enough, we can be happy to receive any final, running system that meets the requirements. It’s OK if we get a different one each time! Programmers are used to mandating more determinism than strictly required by their development and maintenance processes, because they aren’t used to writing sufficiently constraining specifications/programs. The earlier SQL example is a good one: because we don’t trust the database engine to choose the right data structures and algorithms, we worry about changes to the subsystem that plans query execution, but what if we annotated our queries and indeed our whole programs with performance requirements instead? Then nondeterminism becomes desirable because sometimes the programming tools find new and better, faster implementations and drop them in without needing to bother us!
The underlying issue is that programmers worry (justifiably) that some important characteristics of the final system can’t be predicted from the source code alone. Yet, because those characteristics are important, we need to make sure we confirm they are suitable. The most common tool is testing, subjecting the generated code to many scenarios and checking it behaved properly. Over time, developers build confidence in even the parts of generated systems that those developers didn’t write themselves, by running many tests over many versions of the program. If a clever programming tool completely changes up those aspects, we have to restart the confidence-building exercise.
I want to emphasize the two big changes to this flow that I’m recommending. The first is to write specifications so precise that literally any realization of them is acceptable. The thought experiment is for, say, a company building a product to imagine that its biggest competitor gets to write any program that meets the specification. The second important change is to rely on machine-checked mathematical proof that a generated program meets its specification. Now we need not rely on testing to find internal bugs in the generated code, as testing covers only particular execution scenarios, while a proof covers all of them. The risks that remain are in the specification, perhaps most importantly in how we characterize the other systems that ours interacts with – so testing should be focused on that interface boundary, and it can be done against a specification that happens to be executable, not the generated implementation. We no longer need to treat e.g. a tricky concurrent data structure that is purely internal as highly suspicious from a bugs standpoint. This shift is similar to the one that happened with programmers trusting the implementations of higher-level programming languages (though there’s no need for trust, as compilers are a great subject for formal verification).
Another concern came up for having tools choose data structures automatically. How does a program evolve over time if the data format keeps changing, leaving prior databases obsolete? This problem is actually addressed pretty naturally: part of the specification for the next version of a program is that it is able to begin with the old contents of a database, where now the specific format of that database is part of the specification of the new version. The code-generation tool may now either keep the database format the same or generate a migration to upgrade to a new representation. (Note that this concern helps us notice a wrinkle of needing to save generated data schemas in version control or similar, even if they were produced automatically.)
Feasibility of Specification and Verification
Some concerns were expressed about scalability of such methods to very large code bases. It’s important to keep in mind which measurements of size we should worry about. It would be strange for a conventional project to measure code size by the amount of machine code generated by compilers. Instead we measure source code, which is checked into version control. Similarly, raising the level of abstraction, we should be worried about the size and maintenance complexity of specifications. Different programs may have vastly different size gaps between specifications and machine-executable code. We’ll have to see how the specifics turn out, but one orienting principle I’m comfortable asserting now is that such a gap often corresponds to the sophistication of performance optimizations in a program (which shouldn’t also be in the specification), so the gap is likely to be widest in domains with lots of attention to performance.
Some readers were skeptical that the LLM-style experience of getting a pile of complex code written on command can ever dovetail with high confidence in correctness – and I actually agree! I’ve argued that deep learning is better understood as a generalization of search engines than as a “reasoning engine” in the colloquial sense. Coding agents are doing something very similar to copying and pasting from existing code bases into a new one, losing the lineage of vetted good ideas. Instead, I’ve already argued for combining reuse of flexible components with AI code generation, where that generation now just needs to reference components by name. The novelty density of all software worldwide is much lower than the novelty density encountered examining all the parts of a single system, and we should be taking advantage of that low novelty to share carefully vetted code across projects. It should dramatically decrease the program-specific reasoning and proof that needs to be carried out. The effort to build, specify, and verify the components scales well with their potential many uses.
Another dimension of skepticism was the effectiveness of formal-verification tools in checking whatever code has been produced. There is a definite tradeoff between accepting a buggy program or failing to validate a correct program (see our past discussion on undecidable program analysis). In cases where the stakes are low enough, it may make sense to adopt a flow that occasionally lets a bad program through, if it enables more development velocity and creativity by coding agents. However, I personally most favor methods that don’t separate code generation from verification. Correct-by-construction techniques interleave correctness reasoning with all steps of writing code, and I’ll have much more to say about this approach in upcoming articles.
Coming up with a sufficiently constraining specification can be hard and error-prone work. Familiar quality-assurance activities for software may switch to specifications instead, including running specifications against many test cases. Tools for simulation, debugging, code review, and so on can also be very helpful for specifications – and all the above practices are actually already common among users of formal-methods tools like proof assistants. However, I would say most engineers not familiar with formal methods are much too pessimistic about the paths toward high-quality specifications. The reason is that most specifications apply to components that ought to be internal to larger systems, and end-to-end verification of full systems catches specification mistakes in internal components very reliably. For instance, a programming-language implementation is tough to specify in isolation, as we need to legislate exactly what each language feature means, but when that language is used internally in the proof of a larger system, we force ourselves to catch any language-design mistakes that are consequential, falsifying what we hope is a simpler top-level specification of an application, and the language definition becomes untrusted (in the good sense of not being assumed correct). There’s also a handy bonus for catching certain security bugs by proving almost any interesting specification about a system.
We can also keep benefiting from LLMs and similar future tools. Coding assistants can be used to write specifications that are then code-reviewed, tested, and so on, at the level of unambiguous specifications. There is an established research area around programming by example, and such techniques could be used to help write specifications automatically from input-output examples or even, with AI assistance, “user stories” that spell out in English ways that programs should be able to be used. The point is that AI can make mistakes, but the final quality assurance is done against an unambiguous specification (which persists in version control, while natural-language dialogues may not).
Aspects of the pushback about nondeterminism of code generators do indeed sound like trouble to me. I wrote previously about how nondeterministic specifications can promote security vulnerabilities through so-called side channels. It also isn’t hard to see how getting the same answer every time can be helpful, for instance in reproducing data analysis from scientific experiments. In such cases, we can make sure that top-level specifications are deterministic, though it may remain useful to allow systems to be built out of components with specification nondeterminism that is hidden well at the system level. A great example is a low-level memory allocator that assigns memory addresses to different pieces of data, where higher-level code is written carefully not to reveal which addresses were assigned. It pays off to allow new versions of the allocator to introduce clever new algorithms that affect address choices.
There was also a question about whether specifications are just pseudocode, and I think they probably aren’t. That terminology usually implies some use of natural language to explain important behavior, which isn’t compatible with truly reliable automatic programming.
Remaining Questions
One interesting question I received was about the place of undocumented features in software that is regularly regenerated. That is, conventional software ships with incidental features that the developers may never have meant to promise to retain indefinitely, and yet users come to depend on them (as laid out in Hyrum’s law). If regeneration can change such incidental features arbitrarily, users may repeatedly be disappointed. For now, I think my strongest response is that undocumented features are bad, and automation may be able to help us avoid them! However, it’s worth thinking about the consequences of users increasingly becoming AI agents themselves. One of my earlier articles analyzed how the problem of ensuring happy users becomes easier then, for instance because new releases can be checked against the code of known users, to make sure they remain satisfied in all possible scenarios. Achieving a similar benefit for human users remains an interesting software-engineering research question.
Complicated systems must often be debugged in the field, as much as we may hope broad formal verification catches all defects. Some bad behaviors only emerge at scale in real environments, which may include components not yet specified or verified. Generated code can still be provided with, for instance, mappings of running code to the parts of specifications that determined it, along with whatever other annotations best support debugging by humans or machines. Indeed, the quality of debugging collateral could be mentioned explicitly in a specification! However, the details definitely constitute an independent research challenge.
Another interesting comment was about how the world and the connections between its pieces seem on an unstoppable upward trajectory of complexity. Methods based on code generation from unambiguous specifications may hit an applicability wall, past some world-complexity threshold. It’s interesting to speculate about how increased adoption of AI may change this phenomenon. On the one hand, “smarter” AIs may go even further in designing complex, society-scale systems. On the other hand, the selection pressure to enable efficient reasoning by AIs may motivate them and us to create bubbles of improved legibility within which economic systems and reasoning systems are codesigned. The world may seem to grow increasingly complex and illegible to humans while AIs are actually improving their ability to keep up!
We all see how amazingly effective LLM-based coding assistants have become, even if it can be hard to build confidence that they wrote the programs we really want. There is an even older tradition of research in program synthesis. I think there’s a lot of exciting technical work to do to draw on these starting points and create the most effective systems for automatic programming. However, it was an intentional omission not to go into more detail in the prior article, as I’m going to need multiple articles worth of content to do that subject justice; stay tuned. For now, just imagine that some reasonable notion of mathematical program proof is fixed, with ideally one standardized trustworthy checker, opening the door to a variety of methods that produce proofs (in the style of proof-carrying code).
I do want to tease now that I see performance of logic-based automated-reasoning tools as a major bottleneck holding back the area. At a minimum, we need these tools to keep up with deep learning-based tools that may be writing code creatively. A major theme of future articles will be full-stack performance engineering to improve logical reasoning and code generation. In fact, I hold out hope that logic-based alternatives will be able to run even faster than purely LLM-based methods, even if LLMs are baked into custom hardware, because of the inherent performance bottlenecks of deep learning.
Next, though, I want to turn to perhaps the hardest case of complete-enough specification being discussed today: AI alignment, the study of how to build flexible automated decision-makers that we should believe will respect our values and not harm us in surprising ways. My impression is that the conversation so far leans very much on thought experiments not connected to implementations, somewhat justifiably if we may (?) not yet have AI powerful enough to exercise the alignment challenge very thoroughly. I’m going to analyze the problem from more of an engineering perspective, grounded in experience building and maintaining significant proofs of system correctness. The gimmick will be thinking of human brains as a legacy system that is worth engineering around if we can, especially if it must be mentioned in the top-level interface of a system.