Comment by jimmaswell
10 hours ago
It wasn't code worth formally verifying, but even your description beats almost any programmer's first pass. With how good it is at finding bugs if you ask it, I have little reason to doubt its output.
10 hours ago
It wasn't code worth formally verifying, but even your description beats almost any programmer's first pass. With how good it is at finding bugs if you ask it, I have little reason to doubt its output.
> even your description beats almost any programmer's first pass
Sure, but having access to merely mildly superhuman programming ability still doesn't make using C a good idea.
In the real world, I'd say the 90% of the C code written is somewhere between "worthwhile to spend extra effort to detect and avoid memory errors" and "worth formally verifying".
Sure, for prototype sized codebases it might be able to handle finding mistakes a fresh grad might easily make, or even that memory bugs aren't a big problem - but in my experience it happily adds memory bugs to large codebases and multithreaded code (that I think an experienced human could easily spot tbh).