Ferrocene is an exciting opportunity for the safety critical space which is dominated by MISRA C, Ada / SPARK, and similar.

Having AdaCore as a collaborator gives me great hope that Ferrocene will succeed and raise the bar for Rust standardization and language maturity.

I don't see MISRA C as comparable to SPARK in this space. MISRA C is more like a style guide for writing less awful C.

There are huge swathes of MISRA which forbid things which not only aren't possible in Rust or SPARK, they'd probably make a lot of real world C programmers shake their heads in disbelief too. For example MISRA tells you not to put switch labels within blocks started by another switch label. Most C programmers probably had no idea they could do that, which is fine because they shouldn't. In experiments these MISRA rules don't trigger - nobody is actually writing the sort of C that's forbidden.

There are also a bunch of MISRA rules which just seem like style preferences, in experiments these don't seem to contribute to improved software correctness, the "bugs" identified by these rules don't interfere with correct program behaviour. Enforcement of such rules tends to breed resentment from programmers.

MISRA isn't useless, but that's actually an indictment of our industry. This very low bar is still tougher than a lot of code people are actually using. It's like you find out that your country's fire regulations only require a nightclub with 500 drunk people inside to have one working fire exit... and then discovering most clubs in the country don't meet this inadequate standard anyway.

I can't vouch for its accuracy, but https://github.com/PolySync/misra-rust seems to very much agree with you.