Automatic Programming Should Be More Like SQL

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 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.