Rewrite All the Code, All the Time

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, bu…