Absolutely, but do you think that rewriting billions of lines of C code in Rust is the best, most cost-effective way to increase confidence in them? Also, using verification tools can be done much more gradually (say, function by function) than rewriting in a new language (which may require a lot of ffi if done piecemeal), and there's no need to fear new bugs.
> Besides, most safe languages for embedded use (SPARK, etc) get their safety by disallowing dynamic allocation, which is great for avionics systems and not so great for libc or any consumer or server software.
True. I don't actually suggest using SCADE or SPARK for libc :) Astrée wouldn't work, either, as it also assumes no dynamic code allocation. But something like SLAyer (a tool by MSR based on proving separation logic properties through abstract interpretation) or Facebook's Infer should. I would guess that making those tools work well on more and more real-world code would be a much smaller undertaking than rewriting in Rust and proving no new bugs have been introduced.
I'm generally skeptical of significant, real-world, bottom line benefits new languages provide, but Rust has convinced me that, at least potentially, it can have some very significant benefits over C. But a wholesale rewrite of a near infinite amount of code, much of which may work well enough, plus the risk of adding new bugs in the process, without the means to detect them??? That's like draining the ocean with a spoon in the hope of finding a sunken treasure. Software engineers often speak of using the best tool for the job; rewriting vast amounts of code (with very incomplete test suites) in a new language is certainly far from the best tool for the job of increasing confidence in its correctness (unless a particular piece of code is buggy beyond repair).
Same goes for physical infrastructure, BTW. If your infrastructure is old and you fear some bridges may collapse, you inspect them all. You rebuild the crumbling ones and strengthen those with cracks. What you don't do is rebuild all the bridges in the country. That's not only wasteful and comes at the expense of new bridges you could have built, but may end up increasing the danger in some cases, rather than decreasing it.