This is true. But it has some weird gaps that make it difficult to express fundamental things in the low-level systems world without using a lot of “unsafe”. Or you can do it safely and sacrifice a lot of performance. I am a fan of formal verification and use it quite a lot but Rust is far more restrictive than formal verification requires.

Rust is a systems language but it is uncomfortable with core systems-y things like DMA because it breaks lifetime and ownership models, among many other well-known quirks as a systems language. Other verifiable safety models exist that don’t have these issues. C++, for better or worse, can deal with this stuff in a straightforward way.

> without using a lot of “unsafe”

You are allowed to use a lot of `unsafe` if you really need to. How much `unsafe` do you use in C++?

> it is uncomfortable with core systems-y things like DMA because it breaks lifetime and ownership models,

Sure, it means it can't prove memory safety. But that just takes you back to parity with C++. It feels bad in Rust because normally you can do way better than that, but this isn't an argument for C++.