You are projecting your own misunderstandings and confusion onto others.

Calling safe Rust “sound” is meaningless at best and misleading at worst. You cannot seriously test soundness without a formal model and a complete, stable list of undefined behavior. full safe Rust has no formal model, no complete stable list of undefined behavior, to assert that full safe rust is sound is absurd to begin with. keep "not even wrong" to yourself. Is your understanding of Rust’s soundness based entirely on wholehearted belief in Rust’s advertising claims, without even the slightest examination?

“Safe Rust is sound” is an outrageously false claim.

The claim that the guarantees Rust provides are sound is a false claim on the level of a declaration announcing the invention of a perpetual motion machine. You are not merely repeating Rust’s advertising claims; you are producing an absurdly strengthened version of them, claiming that “the guarantees Rust provides are sound” — a statement that even the rust-lang.org front page does not dare to make.

The closest thing one can find right now that is related to proving Safe Rust sound is RustBelt.

The language RustBelt claims to prove properties about is a rust-LIKE language, an APPROXIMATION to a subset of Safe Rust, with a SIMPLIFIED memory model. There is a HUGE GAP between that and the actual memory model.

RustBelt certainly did not prove that a subset of Safe Rust is sound, let alone full Safe Rust.

There is simply no proof anywhere that full Safe Rust is sound.

Rust’s advertisements — original text:

1. “No matter what, Safe Rust can’t cause undefined behavior.”

2. “Rust’s rich type system and ownership model guarantee memory safety and thread safety, enabling you to eliminate many classes of bugs at compile time.”

The first one is outrageously false claim.

The second one is another outrageously false claim. The funny part about the second claim is that array bounds checking is part of memory safety, yet it is handled by a runtime mechanism, not purely by the type system and ownership model as advertised.

These days, Rust memory-corruption CVEs are easy to find online. Given how obvious and readily available the evidence is, it is astonishing that they still have the audacity to make such an outrageously false claim: that “Rust’s rich type system and ownership model GUARANTEE memory safety and thread safety — enabling you to eliminate many classes of bugs at compile time.” The claim is not only easy to see through at a glance, but also contrary to basic engineering intuition. Yet the truly bizarre part is that many people actually believe it, even though the counterevidence is extremely easy to find.

Anyone with even a modest amount of real-world software-engineering experience—so long as they still retain a basic instinct for practical engineering, not necessarily exceptional talent or deep expertise—would, upon hearing that a practical subset of a practical programming language has been proven sound, immediately feel as though they were being sold an absurd perpetual-motion-machine claim. And yet, the whole industry remains indifferent toward Rust’s outrageously false claim.

In a practical engineering language, constructing a safe subset whose soundness can be proven is trivial. The hard part is constructing a PRACTICAL subset of the language that can also be proven sound. For now, this task seems hopeless.

Considering that full Safe Rust has never been proven sound, is the safe region of Rust really a PRACTICAL subset of Rust? I do not think so. It is clear that Safe Rust does not have enough expressive power to write arbitrary code, which is why there are so many unsafe regions and chained unsafe dependencies across the entire Rust ecosystem.

There are three problems:

1. Array out-of-bounds safety 2. Memory safety 3. Concurrency safety

Each problem is at least an order of magnitude harder than the previous one.

What is Rust’s strategy for handling these problems?

For array out-of...