| > Formal methods don't eliminate wrong or insecure results. Yes, they do. That's the entire purpose of a proof. Of course formal methods cannot prevent or even detect wrong specifications, but that's no different from generated code either. > Using formal methods slows you down compared to things like testing which can get us most of the way there in less time. But that's the point - formal methods are slow if people have to apply them. Automated theorem provers exist and can work on generated ASTs, so why not add the step and create a hybrid system that verifies the generated result? >> Instead of turning the uploaded image into a mosaic as intended, the generated code simply creates a fixed-size black-and-white checker-board pattern > It worked fine for an image I just tried. Just like the prompt it "convert[ed] the image to a 32x32 mosaic." There was no checkerboard, but it may be worth noting that it converted transparent pixels to black. The code may have been changed - it works for me now, too, when before it definitely didn't. |
A wrong specification can give you a wrong or insecure result. That was my point. Formal methods aren't a sliver bullet and your system still needs to be robust to failures.
>so why not add the step and create a hybrid system that verifies the generated result?
Because the time spent writing a specification is time wasted if there ends up being no issues with the generated code.