Bounded model checking has changed things. C on its own can't solve these problems. Likewise, Rust on its own -- while it can solve memory errors -- can't demonstrate safety from all errors that lead to CVEs.
Practical formal methods using a tool like CBMC can make C safer. The existing code base can be made safer without porting it to a new language or using experimental mechanical translation. This isn't just something for C. Such tools exist for many languages now, including Rust, so that even Rust can be made safer.
> The amount of people using stuff CBMC is like trying to boil the ocean.
That's like saying, "Getting everyone to use Rust or TDD or X is like trying to boil the ocean."
It's impossible to solve all things for all people at once. But, that doesn't mean that we can't advocate for tooling that can be used today to build safer software. This goes beyond C, as such tools and techniques are being ported to many languages and platforms.
Rust is a solution that works for some people. Modern C with bounded model checking is another solution that works for some other people. I'm certainly not going to change the minds of folks who have decided to port a project to Rust and who are willing to spend the engineering budget for this. But, hopefully, I can convince someone to try bounded model checking instead of maintaining the status quo. Because, the status quo is where we are with projects like the Linux kernel. Linux may pay lip service to Rust folks and allow them to write some components in that language, but the majority of the kernel is still in C and is not being properly vetted for these vulnerabilities, as we can see with the stream of CVEs coming out weekly.
> WG14 can solve those problems, they decided it isn't their priority to fix C.
WG14 must maintain some semblance of backwards compatibility with previous versions of C. It's no good to make a feature that breaks older code. This happens from time to time -- old school K&R C won't work in a C18 or C23 compliant compiler -- but efforts are made to keep that legacy code compiling, for good or ill.
Yep, but we have to deal with what we have. For better or for worse, C remains where it is. We can either use process and tools to improve existing C, or throw our hands up.
I prefer to work toward fixing what is. We are unlikely to see things like array slices in C, and even if such features were added, this does nothing to fix the billions of lines of legacy code out there.
Practical formal methods using a tool like CBMC can make C safer. The existing code base can be made safer without porting it to a new language or using experimental mechanical translation. This isn't just something for C. Such tools exist for many languages now, including Rust, so that even Rust can be made safer.