Comment by pron
20 hours ago
I find this discourse about AI and formal verification of software very confusing. It's like someone saying, let's assume I can somehow get a crane that would lift that vintage car and place it in my 15th floor apartment living room, but what will I do with my suitcases?
All the problems mentioned in the article are serious. They're also easier than the problem of getting an AI to automatically prove at least hundreds of correctness properties on programs that are hundreds of thousand, if not millions of lines long. Bringing higher mathematics into the discussion is also unhelpful. Proofs of interesting mathematical theorems require ingenuity and creativity that isn't needed in proving software correct, but they also require orders of magnitude fewer lemmas and inference steps. We're talking 100-1000 lines of proof per line of program code.
I don't know when AI will be able to do all that, but I see no reason to believe that a computer that can do that wouldn't also be able to reconcile the formal statements of correctness properties with informal requirements, and even match the requirements themselves to market needs.
What I'm trying to say is that a machine that can reliably write a complex, large piece of software and prove its correctness - somethng that, BTW, humans are not currently capable of doing - is also likely a machine that can do that from the prompt: Write a piece of software that will be popular among women aged 35-65, let alone "write a spreadsheet that's as powerful as excel but easier to use". Of course, once that happens, the market value of any such software will drop to zero, because anyone could give such a prompt. In fact, there would be no need for software as we know it because the AI could just do what the software is supposed to do (although perhaps it would choose to create an executable as an implementation detail).
What I see is people spending a lot of time imagining how we would work with an AI that could solve some huge problems and at the same time fail to solve easier problems. I don't understand the point of the exercise.