> There's no fundamental reason why all the checks applied by say, a Rust compiler, couldn't be applied to a piece of C code.
I've certainly thought about how to improve my C++ after internalizing Rust. Unfortunately I've come up with very little. For every implementation of a Rust safety, I've come up with a way to easily (accidentally) break it.
So in the language, while I'd love to see it, I'm not so sure.
Now, if we can just get "a sufficiently smart compiler", then that'd be great. But that's rarely how that works. (cf. https://wiki.c2.com/?SufficientlySmartCompiler)
I've not looked much at formally proven code, but for such code, sure. Note that there are plenty of examples of bugs in formally verified code, too. Partly this is because one formally verified the wrong thing. And aside from that I understand that there are reasons you can't "just" add formal verification to whatever project you have.
Maybe AI can write prefect assembly directly. Then we can all stop arguing about languages.
But in any case, if you want to make the case against my "nobody can write safe C" (or C without UB), and the argument is that they can, if an AI verifies every line. Then yeah, sure. But 1) who was actually writing the code, then? And 2) to the extent that the human was involved in writing the C, they probably made things worse, not better.
Even for AI coding C, there just needs to be one missing thing in the LLM's context, and a buffer could overflow. But for whole classes of bugs (though not all), the difference between Rust-without-unsafe and formally verified doesn't matter. I.e. you don't need formally verified against memory safety if it compiles, and there was no `unsafe` use.
> Gotta have developer velocity, right?
Not having AI at least review the code delta before pushing a release I would say is misconduct, today. It's the equivalent of editing your Perl cgi-bin in an editor live on the production server. That's not "production".
> pick a random open source project,
This is what I mean by not being "production". I won't judge anyone live-yoloing their blog, or "it works for my use case, it's GPL, provided AS-IS don't bother me", which is perhaps most opensource. You don't care if it works? Fine.
But you do care if it works, and/or is safe, and you push releases without AI review: yer fired.
Yes, we have to get from here to there, and I'm not saying release freeze until the entire codebase backlog has been AI-fixed, but yes today you need to have AI review the release delta. Ideally pre-commit.