> If the tooling for verifying C is really so good, why not verify the C parts of the JRE? Then they'd be proven once and for all, and lots of systems would benefit.
I'm going to quote the article again...
> You're more dependent on the decisions made by the language implementers than you think.
When you use Java, you don't have the opportunity to second-guess the choices that produced the JRE. And I think you're not quite getting what I'm saying: I'm not saying that "we should switch to systems which are written more in C", I'm saying that writing systems in C protects you from mistakes in the JRE (which you have no control over) in exchange for exposing you to your own mistakes (which you can control). You can then spend a large amount of time and money developing and verifying your system. The goals and constraints of your project will determine whether this is a good trade-off. I'm certain that Java is preferable for writing the vast majority of web apps, but the web is not everything.
> If the tooling for verifying C is really so good, why not verify the C parts of the JRE?
First, I'm going to guess that an enormous amount of static and dynamic analysis has been done on the JRE. Bugs in it are rather rare these days, given its size and complexity.
However, verification tools are generally not suited to this particular task. Verification tools are better at verifying typical application code, and the JRE needs to do a lot of very unusual operations in order to work. In cases where you'd use verification, you'd also typically use a "safe" subset of C. Some of these subsets don't even permit dynamic memory allocation, or if so, only permit it at program startup.
So, it may actually be more straightforward to deliver a working Mars rover in C than it would be to deliver a verified JRE. Neither task is easy.