Much of its purported virtue seems to be mostly lore and myth, and doesn't keep its promises under close inspection and scrutiny.
For example the "Rustonomicon" is only half finished and doesn't have that much real insight that couldn't be gained from a lot of basic-ish rust tutorials.
The memory model is not propery defined and only kinda sorta borrowed from C++ as the article mentions.
The borrow checker has only been formally specified and veryfied in a much simplified form and only very recently [2] ,with the actual model "just being what the borrow checker implementation does".
Having a fancy datalog based borrow checker is cool, but I'd much rather have a formal specifiation of the semantics.
Rust took the big bang approach of building everything at once, implementing stuff first without any formal semantics and just floating on an iceberg of implementation definedness, with endless discussions on how things COULD be formalized.
That's pretty much the antithesis to rusts safety philosophy; it's teaching water but drinking barrels of wine. It wants your code to be well defined and follow its rules, but its rules are completely arbitrary, not properly defined nor written down.
I wish instead they had just started with a small borrow checked core language, and grown it from there, like described in Guy Steeles talk on "growing a language" [1].
I feel that Zig is doing a much better job in this regard, they have a tiny well thoughought language with a rigorous semantic description, and a good reference document.
I'm sure it would be much easier to add a borrow checker to the well-defined-ness and correctness of Zig, than to make Rust well defined and correct.
Super friendly community though. Who knows, maybe someday the language that people think rust is, will crystalize from that community through their collective effort, like a self fulfilling prophecy.