Comment by layer8

> realizes that the fix is incorrect because of sloppy thinking

If the domain expert doesn’t understand the generated code, they can only discover incorrect logic by specific examples (specific inputs), which is usually impossible to do exhaustively. The programmer, on the other hand, can see incorrect logic directly, generalized over all possible inputs and states. It’s the difference between testing and proving correctness.