True, but C programs that follow the same structure would require about the same amount of annotation. A language can force you to write programs in a way that makes some properties easy to prove, but if you write them in that way, they can be easy to prove in any language. The difference is that instead of rejecting a different kind of program, the analysis will fail to prove, at which point you can either add more annotation or restructure the code to make it easier to prove.

They need much more due to C´s semantics, that is why there are companies like the one on this thread selling verification services and tooling.

It is also the reason why Microsoft has acknowledged their idea of lifetimes checker did not went as well as planned, and they had to rethink it,

https://devblogs.microsoft.com/cppblog/high-confidence-lifet...

For arbitrary code, which is precisely my point. Code written in C in the same style as Rust is no harder to analyse than Rust code. What a new language can do is reject code that's not easy to analyse. It's code that's not written in that way in C that's hard and requires either more annotations or a restructuring (which may still be easier than a rewrite in another language).

It's a good thing all developers in all groups on all projects at a company always conform to the same style in the real world. Otherwise the plan for annotating C might run into some stumbling blocks.

And it's also good that migrating a codebase to a new language with questionable prospects carries no risk or cost. Otherwise its adoption rate could disappoint.