I'm mostly responding to the middle third of the article that IMO interprets the word "correct" in an academic way that, IMO, is unanchored to how, to a rounding error, software is written:

> "Even simple versions of the approach are intractable in the very precise sense of computational complexity theory if we are concerned about generating code that is correct." (Then 5 paragraphs about that being pspace-complete.)

The notion of correctness used in the article is a verified property. My point is probably less than 1% of the programmers on this site have ever verified their code in that sense, especially since they left a university setting. Instead, most commercial developers write tests based on their domain knowledge as developers and some limited understanding of their company's business domain... if at all. Which LLMs can also do.