Can chatbots craft correct code?

I recently attended the AI Engineer Code Summit in New York, an invite-only gathering of AI leaders and engineers. One theme emerged repeatedly in conversations with attendees building with AI: the belief that we’re approaching a future where developers will never need to look at code again. When I pressed these proponents, several made a similar argument:

Forty years ago, when high-level programming languages like C became increasingly popular, some of the old guard resisted because C gave you less control than assembly. The same thing is happening now with LLMs.

On its face, this analogy seems reasonable. Both represent increasing abstraction. Both initially met resistance. Both eventually transformed how we write software. But this analogy really thrashes my cache because it misses a fundamental distinction that matters more than abstraction level: determinism.

The difference between compilers and LLMs isn’t just about control or abstraction. It’s about semantic guarantees. And as I’ll argue, that difference has profound implications for the security and correctness of software.

As I wrote back in 2017 in “Automation of Automation,” there are fundamental limits on what we can automate. But those limits don’t eliminate determinism in the tools we’ve built; they simply mean we can’t automatically prove every program correct. Compilers don’t try to prove your program correct; they just faithfully translate it.

This is an excerpt from the Trail of Bits blog. You can read the full post here.