On software carpentry

tl;dr: “Beware of bugs in the above code; I have only proved it correct, not tried it.” –Donald Knuth

We call ourselves software “engineers.” Yet any sincere “engineer” who wrote more than 10,000 lines of code will tell you “engineering” has very little to do with what we do. We’re mostly duct-taping things.

Before building a bridge, a bridge engineer¹ computes stress, strain and deflection in their beams². A software “engineer” just starts writing code. A bridge engineer operates with a safety margin: the bridge should resist 2x to 4x the maximum expected load. A software “engineer” continues writing more code. Some of this code may be tested, for some input values, but that’s about it. A bridge engineer signs off on their design³ and is subject to professional negligence lawsuits if they seriously mess up⁴$^,$⁵. A software “engineer” just ships the code.

The net result of our “engineering” practice? Years later, when that code leaks your phone number, home address and the names of all your family members, the “engineering” company is “deeply sorry.” This happens several times per year now⁶.

A more honest name for our practice should be “software carpentry.” It recognizes that, while we do have a skilled craft, safety calculations hardly enter into it. My thesis is simple (and, I hope, hardly controversial by now): to graduate from “software carpentry” to “software engineering”, it would be sufficient for us to embrace formal verification⁷.

Luckily, in the LLM age, we could actually do this. Formal verification is becoming easier to apply to increasingly larger projects⁸. The first step is to apply formal verification to our less complex software, software with clean interfaces that admits small specifications. In other words, formal verification for our building blocks:

• “this library sorts”⁹
• “this binary zips”¹⁰
• “this is a EUF-CMA signature scheme implementation with no side-channels”

Then, we could push the boundary beyond simple buildings blocks to more complex systems:

• “this query optimizer produces a plan semantically equivalent to the unoptimized query”
• “this consensus protocol satisfies safety and liveness under \(f < n/3\) Byzantine faults”¹¹

If we did so, there’d be many advantages:

1. We can safely unleash AI to optimize our codebase.
   • This requires progress in compiling (say) Lean programs to be faster.
   • Or, it requires what has been referred to as “the final form of software development”¹² to manifest.
2. Folks are barely reviewing AI-generated code anyway. Formal verification can enable them to safely not do so.
3. Instead of tests that cannot cover all executions with all values¹³, we prove all executions perform what we expect them to.
4. Instead of repeated, error-prone (LLM/manual) audits on our ever-changing, large codebases, we can reduce audit scope to the specs, which are implementation-agnostic.
5. Instead of trusting that an imported dependency does something, we don’t; we update our proof after integrating the dependency. If the proof passes, then program only does what the spec says.
   • The only part will be a bit tricky, but doable.

There already is plenty of encouraging work showcasing the viability of formal verification (pre-LLM age):

1. seL4, an entire OS microkernel, proven functionally correct¹⁴.
2. CompCert, a full C compiler, proven to preserve program semantics from source to assembly¹⁵.
3. IronFleet, a Paxos-based replicated state machine plus a lease-based sharded key-value store, with proofs of both safety and liveness¹⁶.
4. Everest TLS stack, a formally verified TLS implementation (miTLS), covering the full protocol state machine, not just the handshake crypto¹⁷.
5. AWS’s use of TLA+, not a proof of an entire system, but industrial-scale application of formal methods to distributed systems bugs at production complexity¹⁸.

As caveated above, formal verification will not be a panacea:

1. Some software can be as complex to specify as it is to implement (e.g., EC2 cloud architectures come to mind).
2. Software evolves, not just in its implementation, but also in its specification.
3. Formal verification rarely covers the full system $\Rightarrow$ bugs creep in in uncovered parts.
   • For example, seL4 had bugs due to timing channels¹⁹.
   • CompCert had bugs in its unverified parts: parsing bugs that produced a bad abstract syntax tree (AST), since the formal verification only modeled compilation from the AST²⁰, but also bugs in its C elaborator, in its Win64 ABI model and in its assembly printer²¹.
4. Formally-verified systems are often compiled with an unverified compiler
5. Formally-verified systems often execute in an unverified environment: the operating systems, the x86_64 CPU, etc.
6. The formal verification framework/language may itself have soundness or completness issues²².

So, if you are tired of being a carpenter whose chairs keep breaking “for no reason,” what other options do you have?

References

For cited works, see below 👇👇