On the topic of "inherently clearer languages", I am a big optimist. One example is that people are much better at dealing with "successes per failure" than accuracy or precision or recall or 9s. Another example is that I've found myself writing correcter faster creativer usefuler queries with this unnamed query syntax:
Animals | where type="dog" | sort age asc | first 10 | cols name picurl shelter breed > puppies.jsonl
Another huge change in my habits has been giving short_names to requirements like
req_3x_is_2x: tripling the cpu cores should at least double the throughput
Then I can reference req_3x_is_2x in a comment or message
Or a more common one is req_mobile_not_whitescreen
Then you can tell the auditorbot to check a random subset of requirements on a random subset of code. Violations quickly go to zero. If the constraints are satisfiable.
Regarding ease of rewriting software, I think the change is real. I never made any real programming languages or databases before, but now I can whip one up in a day or two, that matches all my requirements and is faster! Other people have better examples.
I am curious what exactly makes you optimistic about right proper Formal Methods.
There are a number of dimensions I could mention (and they all get at least links snuck into the article), but one that I feel is underdiscussed is the economic cost of code generation. Assume for the sake of argument that LLM-centric flows will produce fully satisfactory output in the near future (or may already). It just takes a long time to get answers back from AI-coding tools. And the latency is fundamental, given the way that deep-learning models are structured and the way other tools are built on top. Latency will really matter for periodic regeneration of all code relevant to an organization.
My hypothesis is that logic-based methods can also take advantage of highly performance-optimized parallel compute to generate better code (though maybe only in relatively rare but important cases) at orders of magnitude lower cost and latency.
Plausibly, there's a point where coding models and tools get stable enough to not change often, at which point you can do things like make custom silicon to get the speed and efficiency up.
Absolutely true, but the dataflow graphs of this style of solution are fundamentally slow to execute, because they include long sequential dependency chains, as I've written about at more length. Going to custom silicon can improve the constant factors, but I don't think it's enough.
One ridiculously effective method is to tell the AI to mimic the process and checks and style and patterns of $name, to the extent that you can't tell whether $name wrote it. You have to pick someone with a near perfect security track record. Perhaps the author of this post is a good name.
Heh! I've certainly heard about good results using that method, but has there been rigorous evaluation? Is it bullet-proof enough to use with security-critical code? What about in cases where adversaries have crafty ways to bias requirements documents (e.g. they control documentation of libraries being used?), so that they mean the right things to specialists but somehow manage to trigger wonky behavior by opaque AI models?
It is a very flawed method, yeah. If you're going to do something on the level of a onetime system prompt and forget about it, this is the best trick I know.
Adam, you are acknowledging progress on the generator side, but not on the verifier side. Formal specs are great becase we have existing verifiers that are nearly-garanteed-sound. But those verifiers are also extremely limited in what they can handle. And LLMs can also be verifiers! They are much more error-prone, but also a lot more powerful! IMHO, it's silly to insist we only allow pre-AI/pre-LLM verifiers. Instead, we need to acknowledge that we are now having increasingly compelling alternatives that provide new options for expressivity vs soundness trade-offs. The FM paradigm should survive in terms of the general workflow combining an implementation + verifier, the methodology for modular specifications that make thing more accessible to less-scalable verifiers, but without insisting that only legacy specification languages and legacy verifiers are OK. In some particularly important cases, the soundness is critical and we would use them. In others, the expressivity is more important and using less formal language with LLM-based verifiers might be perfectly fine. And if specifications are produced and consumed by the same LLM model, it might be inaccurate to characterize those specifications as being simply written in a natural language - if done right, LLM might be able to be a lot more predictable in how the language is interpreted.
Great points, which I take as drawing attention to the tradeoff between false positives and false negatives in automatic verification. Especially in domains not considered security-critical, we may be happy to accept that a verifier (perhaps based on an LLM) sometimes accepts a program with a bug, so long as it makes the right call most of the time.
There is a subtlety to the question of which verifiers count as "extremely limited in what they can handle." I'm thinking most prominently of general-purpose proof assistants like Lean. They should be able to verify correctness of any program, but the catch is that someone (human, AI, a collaboration between them) needs to write a proof! However, once the proof exists, it is easy to check.
FWIW, I totally agree that we need to change the verifiers to answer the challenges of new developments in AI-assisted programming. So much effort is going into performance-optimizing ML inference, and the extent of similar effort for formal-verification tools is paltry in comparison, setting us up for formal methods as a performance bottleneck. That's why I'm excited about building new hardware-software stacks optimized for formal verification and program synthesis, perhaps hosting symbolic and neural workloads on the same platform with fast interconnect. It's a major thrust of my own present research, and I will return to the subject often in future articles I'm planning.
The chance to take advantage of LLM "internal languages" is a great point, whose consequences I haven't digested yet.
[...] economic forces will push toward simplifying the world in pockets of activity given over to automation – and over time, the fraction of the economy covered by such pockets will grow, and pockets will merge with each other. We should expect collecting unambiguous requirements to get much easier in that world.
I like the direction of this post, having similar interests. However, I think the bubble metaphor is weaker than the rest of the argument, and that there are clearer ways to show why it makes sense to adopt formal methods.
Let's start with the weakness of the bubble metaphor: you don't go into the externalities, limitations, collaboration and upkeep needed to uphold and maintain a bubble. The world is becoming increasingly standardised, discrete, manageable; yet also increasingly convoluted, non-linear, surprising etc. Keeping up the standards sometimes works as if by magic (clock time seems just part of the territory nowadays). I'm lurking in a protocol research group that is looking into exactly things like this, and it is an interesting and tractable area, but also very messy!
For me, the argument is simpler: To get an AI to produce an artefact, that artefact needs to be specified. We have different ways to specify an artefact, from natural language, to unit testing, to linters, to e2e acceptance test, type-driven programming with algebraic invariants, to user feedback and testing. I'm surely missing some. These specifications can be seen as constraints in program-space, creating an intersection where variations of the produced artefact lives. The more constraints we have, the better. The "harder" our constraints are (as in not budging, not being flexible), the better. Formal specification is a way to make natural language harder, a better constraint. Nuff said :)
In my mind, the reason we don't have pervasive property testing, algebraic laws, strongly typed systems, well-designed programming languages etc, is because adoption requires onboarding, which is costly. I hope ai will change the picture.
Thanks for zeroing in on a tricky idea that I could use help articulating and arguing for. I certainly agree that requirements that impose additional constrains make it safer to use automatic code generators, and the broader economic context does not need to change to make that statement true.
I think it is a fascinating question for study whether increasing uptake of AI will reduce the tendency of the world to become "increasingly convoluted, non-linear, surprising" in your words -- partly because those qualities make it harder to apply AI effectively. Are you personally betting on convolution and surprise increasing? I don't mean that humans will be surprised; it's likely we'll find a world of increased use of AI mind-bending. But will the AIs find that surprise is high and increasing?
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. It has become a mainstream prediction that software code as we know it will become a throwaway byproduct of automated workflows. I argue here that the default generative-AI approach of today is not up to the challenge of full automation (without required human oversight), because it consumes requirements as natural language, an inherently ambiguous format. Instead, formal specifications in logic have an important role to play, to support routine regeneration of all code used by some organization, without auditing by people.
My last article argued that, contrary to popular doom and gloom about LLMs finding security vulnerabilities at unheard-of speed, we have a great opportunity to improve software security. The catch is that it involves significant changes to development techniques to take advantage of formal verification. Sure, in theory, it would be great to release only programs that have mathematical proofs of meeting the most stringent security requirements. But there is so much code already out there and so few developers trained in driving the formal tools. Are we stuck with no path to better practices?
I’m going to make the case now for an even broader opportunity. We need to stop thinking of production-ready code as a scarce resource. It may take a few years to get the tools up-to-snuff, but we’ll reach a point where the cost of ongoing reimplementation of significant code bases drops to the levels associated with SaaS subscriptions today. Let’s start preparing ourselves for how software should be built and maintained in that world. Whenever there are innovations in security concerns that all applications’ designs should address, we will be able to regenerate all of their code to comply. When new algorithms for familiar problems are invented, the cost should be near zero to regenerate using those algorithms, even if they require small customizations. All sorts of different requirements dimensions are fair game for incorporating in fairly frequent regeneration of all code in a project.
The idea that legacy code will steadily lose value, as it becomes easier to replace automatically, is becoming pretty mainstream, at least in the Silicon Valley hype ecosystem. In fact, the strong version of the thesis, which I endorse, is that code as we know it will become a throw-away automatic byproduct of the real long-lived artifacts, joining formats like assembly language that we mostly think of in that way today. I’ll start by making my version of that case. However, there will be a twist! I don’t think the story is nearly all about generative-AI methods that are popular today. Instead, formal methods will be crucial to realizing the strongest version of this idea, because they enable truly automatic generation of full code bases without human oversight.
Automatic Programming
It’s not nearly a fringe viewpoint today that programming will soon be done almost entirely by AI code generators that start from natural-language requirements. The goals and methods line up to an extent with the longstanding program synthesis area of computer science, though the details have been shaken up a lot by machine learning relatively recently.
A good book to help understand the present situation is The Computer Boys Take Over. It covers the rise of “automatic programming” and programmers’ indignation at having it commoditize their skilled labor. A quote from a conference report covers the idea that “managers can now do their own programming” (though the quoted writer expressed the concept with skepticism while noting it was in the air).
However, there’s a catch: the quote is from 1962! The subject is the introduction of the first high-level programming languages and compilers, which automate the tedious writing of code processed directly by computer hardware. Programmers today just take for granted that they write in high-level languages, and pushback against AI coding tools has to do with the writing of those programs, not the ones that 1960s programmers were worried about being generated automatically. I would argue that the lesson we should learn is that the level of programming abstraction in software development is constantly rising, and we should not be surprised to see a step change toward an even higher abstraction level today. Indeed, David Parnas made that observation no later than the 1980s.
Let me spell out the framing a little more. There are many different ways to describe a given program. We get used to thinking of some languages as for writing “implementations” (e.g., Python) and some for writing “specifications” (e.g., various flavors of formal logic). However, I’ve found such a hard-and-fast distinction to be counterproductive. Let’s just think in terms of lower- and higher-level ways to describe functionality.
So the overall idea is that we want to describe programs in as concise, high-level ways as possible. Instead of storing conventional code in repositories, we would prefer to store the highest-level description of requirements that we can get away with, where available tools reliably automate the rest of bringing the desired program to life. Some nonfunctional requirements may change, in which case we can relatively simply fold them into the requirements and redo generation. Security is a good example that the last article covered, with examples like taking high-level secrecy policies and applying them on top of newly discovered vectors whereby programs can leak information. Another great example is performance, where I’m actually pretty surprised at how rare it has been for practical programming languages to support annotations that spell out performance requirements, so that it’s a compile-time error if code can’t be produced that is fast-enough, uses little-enough memory, etc.
In general, the game is to capture requirements unambiguously enough that any program meeting them will be acceptable, allowing truly automatic regeneration of running systems after light-to-moderate requirements changes. A thought experiment might be useful to capture the model. Imagine that some government routinely bids out software projects to contractors, which see each other as bitter competitors. What if every project went to two contractors, one who writes the specification and the other who gets to write any program meeting the specification? A specification gets written defensively, assuming the least-charitable reading by an implementer. In fact, the same specification, or its small evolutions, can be handed to a succession of adversarial implementers, which can, in theory, be an entirely safe way to maintain a program.
If it works, then established code bases of the conventional kind shrink dramatically in value. It becomes unclear that one organization can have an advantage over another on the basis of its stockpile of code written in conventional languages. What matters instead is having the right specifications. We reanimate them in new circumstances just like we recompile code today when libraries it depends on have been upgraded. I like that analogy, too, for connecting to how we might mix in new security requirements or new algorithm ideas, to be applied automatically in regenerating lower-level code from a specification.
Natural Language Won’t Cut It
The trouble is that the mainstream conversation is all about generating programs automatically from requirements in English and other natural languages. I’ve written before about how natural-language processing is perversely hard: not only are there inherent ambiguities that our evolutionary environment didn’t force us to fix, but there is even a strong argument that, to the extent we can think of natural language as “designed” by evolution, it was designed to be difficult to process, for its role in signaling. The related problems are so hard that I doubt we will ever have fully automatic generation of production-ready systems from specifications in natural language – and organizations that fall short of full automation will not be able to keep up in the new economy.
I argue it’s a historical accident that we wound up with today’s deep-learning stacks as the only ones apparently up to this challenge of comprehensive automatic programming. Certain features were helpful in computer graphics and wound up built into GPUs for that reason, and then GPUs turned out to be useful for deep learning. Epic amounts of effort on full-stack performance engineering have gone into the domain, but we can make the same kind of effort to support better code-generation systems.
Let me give a brief set of pointers to my past articles making the case for a different, logic-based paradigm for automatic programming. Deep learning is very effective as a kind of souped-up search engine, but the match with the full process of programming is strained. At a fundamental level, deep learning implies serious performance bottlenecks, and it may also be impossible to prove mathematically that deep learning-based systems always meet our requirements. The power of these systems comes from analyzing large numbers of examples, and, for many domains, we happen to have enough examples only in natural language, but we need not restrict ourselves only to techniques that need to learn from examples. A related idea for automatic programming is curating libraries of flexible, reusable software components, which AI can then invoke by name instead of applying via emergent patterns from training. An even-more-powerful idea is codesigning decision-making systems with the problems they solve, where we should be able to avoid some of the most standard challenge problems for AI, leaving mostly problems that we can solve by generation from relatively compact and unambiguous specifications. While the standard retort to so many varieties of formal methods is that the real world is complicated and hard to specify, economic forces will push toward simplifying the world in pockets of activity given over to automation – and over time, the fraction of the economy covered by such pockets will grow, and pockets will merge with each other. We should expect collecting unambiguous requirements to get much easier in that world.
Why do we need to push beyond the spec-driven development techniques that are being built out today via a variety of tools, taking natural-language documents as “the new source code”? One instructive spec format from this domain is EARS (the Easy Approach to Requirements Syntax). It provides an alternative to freeform requirements as in the following sentence.
As long as the vending machine isn't out of product X, when a customer presses the button for X and inserts payment equal to the cost of X, the vending machine should dispense one X.In EARS, the requirement can be rephrased as
WHILE inventory of product X remains, WHEN the button for X is pressed, WHEN payment equal to the cost of X is inserted, the vending machine SHALL dispense one X.The all-caps words are keywords, delineating parts of a template that has a rigorous formal meaning. The problem is that all the other phrases remain in freeform natural language, with all its ambiguity. An AI code generator can misinterpret those parts, through either innocent misunderstanding or crafty malice.
Tools for spec-driven development will often translate specs at the level of EARS into finer-grained specs, often with multiple steps of increasing precision, taking up significant human time to detect mistakes. We just won’t be able to realize the full potential of rewriting all the code, all the time if we create so many bottlenecks where human attention must be applied. Regenerating based on new requirements should be as push-button as recompiling programs in conventional languages.
Here’s a closing diagram to sum up the narrative of progress that I’m pushing. It involves (1) changing more phases of software development to use languages with clear formal semantics and, partly as a result, (2) moving automation (as opposed to expert human effort) earlier in the development process. Much earlier in the history of software, flowcharts were used as an intermediate program form with unclear semantics, and they were effectively replaced by high-level languages. Natural language-based spec formats strike me as that kind of hybrid beast that we’d be better-off replacing with a proper, unambiguous language.
Conclusion
I’m the kind of optimist who often argued for throwing away all the old code and rewriting it in a better way, even before new AI-powered tools dramatically lowered the costs. When I started graduate school, “everyone” seemed to agree that the x86 architecture had achieved such dominance that serious work on programming tools had to work with x86 binaries – and then we had the rapid rises of both mobile platforms, which sported alternative architectures like ARM that were more energy-efficient; and web applications, which developed their own parallel universe of JavaScript implementations and no distribution of computer-native code. The applications in these ecosystems (and many of the tools behind them) were created basically from scratch over handfuls of years – and they didn’t even have AI to accelerate the process!
The payoff of a reliable flow for rewriting all the code is no longer having an excuse for not using the latest ideas for software quality everywhere. We should be able to take familiar cadences of, say, new software releases and instead associate them with complete rewrites of all code used at particular companies. The key is setting everything up for absolute minimization of the need for human oversight during a cycle of regeneration – and only formal methods seem up to that challenge. It’ll take reengineering of the stack for high-performance inference to work natively with formal logic instead of just linear algebra (though it may work well for the two styles to cooperate), which I started sketching recently (e.g. in discussion of hardware-software codesign that converges the two sides) and which will occupy many future posts here. There’s going to be a lot to figure out, just as the design and implementation of high-level programming languages became a sprawling enterprise.
My next article will suggest one sociological approach to kicking off the virtuous cycle of rewriting a lot of important code.