Formal verification is the next frontier

LLM-powered coding agents have developed faster than I predicted. Tools like Claude Code still stumble on more complex tasks, but a non-trivial portion of the software engineering profession is now automatable. This is great news for the world, since labour cost has been a bottleneck in the proliferation of software.

As the cost of writing software trends towards zero, I think the value of software professionals is in vetting and testing machine-written code. This is not unlike the advent of compilers replacing hand-written assembly, which had plenty of push-back from programmers. This is bitter-sweet: writing all code by hand is fun, but we should not aim to write the same functions for the next 20 years. For many individuals it will be imperative to "move up the stack" and think in broader terms.

The software industry is not yet geared for this phase shift. Having LLMs write thousands of lines of unit-tests is one path to making reliable software, but it is not the best one in my opinion. Unit tests are not the optimal way to write invariants for software. Unit tests essentially sample your problem space to try infer qualities about your program under larger groups of input types.

In my opinion we should be using languages like Lean to make programs verifiable without needing to write tons of unit tests. Although this requires more upfront effort, the result it easier to maintain and quickly evaluate.