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-bounds safety, Rust uses a runtime mechanism to check whether an index is within bounds. If it is not, the program panics.
Rust uses a runtime mechanism, rather than pure static analysis, to tackle the easiest problem among these three. Meanwhile, it attempts to solve the two harder problems — memory safety and concurrency safety — through pure static checking and the type system.
These are the three premises:
Practical engineering languages cannot provide engineering-meaningful guarantees for array-access safety through type systems and static checking.
Practical engineering languages cannot provide engineering-meaningful guarantees for memory safety through type systems and static checking.
Practical engineering languages cannot provide engineering-meaningful guarantees for concurrency safety through type systems and static checking.
This is a strategic engineering judgment about the viable route, not a proof. If you do not agree with these three premises and are not interested in giving ironwall compiler a try, just leave. I am not interested in convincing anyone. If you think these three premises are "not even wrong", keep the hallucination to yourself.
I read some of your comment history, and it contains many vicious and malicious personal attacks. In my dictionary, respect simply means not insulting others. Nobody is entitled to anything beyond that. Before demanding respect from someone, please first ask whether anyone has actually insulted you. Your comment history shows that you have been asking people for more than that, which is out of line. You are not entitled to it.
How about starting with yourself by not making random, false personal accusations based on your beliefs about an advertisement? If you think this is a waste of your time, just leave. Nobody is begging you. Nobody needs your validation. Nobody needs your approval. There is no need to spend so much time writing so many vicious comments, not only on this post but elsewhere as well, if you claim your time is so precious.
Overall, this reply is not merely for you; more importantly, it is meant to clarify my position.