It seems to me that the part about unsafe operations is pretty much still unspecified. It's currently just a short paragraph saying it may cause undefined behaviour and a list of high-level descriptions of those unsafe operations. But what's the exact semantics of those operations? When is it undefined?

The Ferrocene Language Specification has two serious problems: there are very large gaps in it, and what's present is very buggy.

If you pick a small part and look at it in isolation it typically looks quite plausible, but if you try to follow the definitions it very often just falls apart.

Are there some interesting public examples of where the FLS fails?

A year or so ago I read through one smallish section (basically function calls) and filed issues for the problems I found that were easy to write up crisply.

They fixed the easy bugs:

https://github.com/ferrocene/specification/issues/453 https://github.com/ferrocene/specification/issues/454 https://github.com/ferrocene/specification/issues/455 https://github.com/ferrocene/specification/issues/458 https://github.com/ferrocene/specification/issues/459 https://github.com/ferrocene/specification/issues/460 https://github.com/ferrocene/specification/issues/461 https://github.com/ferrocene/specification/issues/463 https://github.com/ferrocene/specification/issues/464

But they didn't try to fill the gaps:

https://github.com/ferrocene/specification/issues/462 https://github.com/ferrocene/specification/issues/465 https://github.com/ferrocene/specification/issues/466

There were a lot more places where I had notes saying "it needs to say more about X" that I couldn't face trying to file issues for.

I think that part of the spec wasn't any worse than average.

I know I'm late to the party, but I still wanted to answer this. Disclosure: I am one of the Managing Directors at Ferrous Systems

I believe you're falling victim ot a common misconception about what the FLS is and what it aims to be. It is - at least as of now - a description of the language that is good enough to certify the compiler. It was never intended to be a spec that describes Rust in completeness - for example, the FLS is absolutely insufficient to implement a Rust compiler. As such, we have no aspirations to completeness in any shape or form. While we get a lot of feedback about pieces that people consider falling short of their expectations, it is expected that there are gaps that Ferrous Systems will never try to fill. The FLS in its current shape is good enough for us.

Now that the Rust project adopted the FLS as the initial nucleus of a spec, I hope that others can contribute and fill the gaps that they need filled.

From experience with these kinds of specs, one might be better off clearly stating things that are left to the compiler implementation (and thus should have no impact -?-on the verifiability of the spec).

This is much bigger news than I think people realise. With the push for more secure systems programming language, having a formal model will enable much more powerful tooling and theorem proving that will help spot, model, or identify vulnerabilities. (There will still be a class of vulnerabilities from when the implementation does not match the specification).

Yeah and at the same time there are efforts to verify standard library using Kani: https://model-checking.github.io/verify-rust-std/

Between this and Bjarne Stroustrup panic leaked email to C++ standards committee members, it's going to be interesting for Rust's future.

While I agree with the huge adoption improvements, there is also a dose of reality check required.

There are several domains where C++ never managed to displace C, and likewise the same seems bound to happen with Rust towards C and C++, regardless of safety improvements.

Khronos API definitions, the whole GPGPU ecosystem including vendor tooling, all major runtimes and compiler frameworks, consoles devkits, are few domains where Rust has yet to have a presence.

All GUI domain seems to be one big state, and that is the kind of place Rust refuses to interact with easily.

That's not true. There are many GUI libraries for Rust.

There are. You can do it. It's just that the language fights you on it.