I completely agree with your assertion regarding the verification tools for C, unfortunately most commercial projects (i.e. not regulated) won't pick between e.g. Frama C and C++ and instead will choose between plain old C and C++, thereby making C a very poor choice.
Nitpick: The idea of your comment is sound, but Frama-C is a C program static analysis framework, not a C subset. You still write regular old C even with Frama-C.
Yeah, but I didn't say pick between Frama-C and C++. I said pick between a subset of carefully-written C with all the tooling one could throw at it and C++. The latter comparison is an easier tradeoff to make than the former. Especially with the tools I mentioned with low, false positives. They'd be serving Google well right now. Among other users.
C has gotten considerably better over the last decade with the wide availability of dynamic analysis tools. Its not particularly difficult to run a project's unit tests under each of the various sanitizers nowadays.
