A few things:
1. There is a spec now, Ferrocene donated theirs, and the project is currently integrating it
2. The team takes backwards compatibility seriously, and uses tests to help ensure the lack of breakage. This includes tests like “compile the code being used by Linux” and “compile most open source Rust projects” to show there’s no regressions.
Ferrocene is a specification but it’s not a formal specification. [Minirust](https://github.com/minirust/minirust) is the closest thing we have to a formal spec but it’s very much a work-in-progress.
It's a good enough spec to let rustc work with safety critical software, so while something like minirust is great, it's not necessary, just something that's nice to have.
Isn’t the Ada spec also not a formal spec?
The most popular language with a formal specification is Standard ML.
I guess this is terminology confusion on behalf of Surac, who probably just wants a specification that is independent of the rustc implementation.