Software 2.0: The Dawn of Anti-fragility

With many recently released models (such as Claude 3.7), everybody and their mother is happy with how it writes code. Still, it is an intermediary step to more significant goals in disrupting software development. We're still doing baby steps. And, possibly, in the wrong direction.

What AI is doing for software developers today is taking their tools and gaining agency in using them, boosting our productivity. However, we delegate the same process we're using to AI: describing the program operationally as a description of steps to do, and then we find issues with it, debug them, and fix them. We do not introduce any additional means to verify our programs make sense, work as intended, or even define explicitly enough what we envision to accomplish. We don't have a specification for the program; instead, we use the implementation itself as a specification.

Is there a way to get a program that works correctly from specification alone? I think so.

Provably correct programs

A fascinating observation called Curry-Howard correspondence links logic to type theory. In computing, it means there is a proof for a theorem if a term of a theorem type can be constructed. A well-known example demonstrating its power is the Four-color theorem, which was proven computationally in 2005, two centuries after its formulation.

It means we can brute force our way or use heuristics to find proof of the theorem about the computation that's verified by the type checker, and it's going to be valid logical proof. As a software engineer, you can think of the proof as a much more potent test form - tests only cover cases and inputs you explicitly test and all possible inputs against a particular property. A simple example would be a theorem stating the associativity of a specific operator, such as list concatenation (++):

∀ lists a,b,c:(a++b)++c=a++(b++c)

It may be evident in this example, but it's not so simple once we start building on it. Any theorem can be used as a building block to prove more challenging theorems, so you get to state-of-the-art mathematics with these tools. The demonstration of it in action can be found in this computerphile video, for example.

A great example of this applied to software development is CompCert - a verified compiler of C. This work took 20 years to formulate and prove, but imagine if we can automate it with AI to be done in 20 hours at some point in the future and make it cheap. Contemplate how much buggy software it will eliminate in one go, probably wiping out the entire infrastructure built around today's programming languages. There are many challenges to this goal, of course, but breakthroughs in AI today make me very hopeful.

You're asking why you haven't heard about it and if it would be great. A steep learning curve requires time and expertise; the prover's work is labor-intensive. So, a greater level of automation can make a zero-to-one difference for the whole domain. I have to mention there are approaches to automation today, such as tactics described in this book: http://adam.chlipala.net/cpdt/, but I think it falls short of expectations because it's still very tough to use even by a seasoned proof engineer.

AI can help us automate writing specs and implementations and find proofs for them, allowing code generation to produce code that can be executed and formally checked for essential properties. So far, it's extremely valuable for edge devices you can't easily update or for hardware production you can't easily recall.

Once we have the power to prove things, we can go further.

I'm certainly not the only one thinking that.

When I was researching state-of-the-art in this direction of AI, I came across papers by:

* Generative Language Modeling for Automated Theorem Proving by Stanislav Polu, Ilya Sutskever of SSI (ex-OpenAI at the time)

This one felt like a dead-end as it used LLM as a proving engine, and now it's a dead end.

• HyperTree Proof Search for Neural Theorem Proving by Meta AI team (Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, Timothée Lacroix)

This one was more interesting, but contrary to Meta's open-source claims, it reveals a subset of the project scope, letting the reader guess the rest.

Software 2.0

We have to go past LLMs to create specialized models to prove theorems. However, when we have it, we can use every tool to assist us with specifications, program generation, and proofs. Going there will make software anti-fragile, allowing us to spend more time envisioning what we need to build, not how. It is a software click moment that will separate the eras of software development.

We can give humanity a chance for massive scientific breakthroughs and truly disrupt the software industrial complex if we find a solution to automating these methods by building expert models and reducing the indirection.