Thank you for an exhaustive answer!

> The difference is pretty important. Getting this certification does not require that the abstract concept of the Rust language is being specified in any specific way.

Sorry, I was being vague. I meant the outcome for "us", the users, creating certified software relying on Ferrocene.

Totally on board with that there is a huge difference for certifying Ferrocene itself.

> The opposite, this means you can use Rust in these places. Even though this work does not specify Rust.

Nice, that's what I was hoping for. We are currently in a project creating safety certified software (in C, as are our other code) and are curiously looking at Rust, partly because of this effort.