>> Much of the world we interact with every day already runs on PHP, JavaScript, and untyped Python that is not verified, not type checked, and has repos overfl

>> Much of the world we interact with every day already runs on PHP, JavaScript, and untyped Python that is not verified, not type checked, and has repos overflowing with bugs and CVEs. Yes, see, that's exactly the motivation for program synthesis (i.e. the automatic generation of programs that are correct with respect to some specification). Human programmers are perfectly capable of producing buggy code on our own. Nobody needs a system that can automatically generate bugs for the programmer to find and fix. We want something that can help us find bugs and fix them, or generate bug-free code automatically (if you can do one, you can do the other). That is computationally hard and that hasn't changed, just as complexity theory hasn't suddenly been rendered obsolete, because of LLMs. Every attempt to get LLMs to produce correct code so-far use an LLM as a generator and then filters its output through a classical verifier, which is subject to all the issues with complexity that arise everywhere in program synthesis (for an early exemplar of that see DeepMind's AlphaCode).