Thanks for your reply but like I said above it's based on a misunderstanding, that program verification and Program Synthesis are one and the same. As far as I

Thanks for your reply but like I said above it's based on a misunderstanding, that program verification and Program Synthesis are one and the same. As far as I can tell the article is not trying to make that claim, either. What the article does that perhaps causes confusion is that it uses the term "Program Synthesis" to refer to one kind of Program Synthesis, specifically, Inductive Program Synthesis. That is Program Synthesis from an incomplete specification, such as a set of examples of inputs and outputs of a target program. Deductive synthesis assumes a complete specification (a complete description of the target program, usually in some formal language). Inductive synthesisers have to [1] search a large, combinatorial space of programs in order to find a program that satisfies a specification. This search itself has typically exponential time complexity and if it is coupled with a formal verifier then you have an at least NP [2] search on top of PSPACE verification. For this reason many inductive synthesisers don't use formal methods to verify candidate programs but instead check the output of a program's execution against I/O examples. That's very much like the software development process you describe, with informal tests such as unit tests. It's still very expensive because of the combinatorial hardness of the program search space. That is what LLMs can't do: they can't do inductive program synthesis on the cheap. Generating programs with an LLM is subject to the same explosive combinatorial search as any other search-based approach: you're generating a large number of programs, until you find one that does what you want. It doesn't matter how you check whether you have the right program: the bottleneck is the search of a huge program space. On their own, of course, LLMs can generate correct programs only by chance, so you do need some kind of verification procedure to check their output, whether it's formal verification or "just" testing. It depends on what guarantees you want. Formal methods can give stronger guarantees while "just testing" can only tell you that a program "covers" its training examples. I'll stop here because I don't want to write a huge comment but there's more things to say about how we ensure program correctness and what that even means in practice and in principle. I think I gave some hints above though. _____________________ [1] Well, ish. There are alternatives, but not very well known. [2] It depends on the approach.