[mccoyb]

My feedback is that both the motivation and the language looks like someone who is confused about several concepts in programming languages.

Safe Rust cannot cause undefined behavior ... static systems do not need to predict all runtime paths, presumably referring to the halting problem and Rice's theorem (or whatever the author intends this to mean, the writing is unclear): these systems prove properties for all accepted programs under a conservative model, which covers all allowed programs within the subset admitted by the model.

The guarantee that Rust provides are sound, and the claim depends on trust in compiler implementation and any `unsafe` code involved in used APIs, etc (which is not uncommon: the same thing is true for Lean's kernel, for instance).

As Pauli said, much of the writing is not even wrong ... many of the language critiques read like transcriptions of vibes derived from AI discussion: "C++ smart pointers with extra steps" -- this is not a serious statement. I'm not even a serious user of Rust, but I know enough about the language design to understand how stupid this statement is.

So the goal seems to be: Java, but without nulls, erased generics, OOP, or the JVM.

Best of luck.

[abecedarius]

I only spot-checked the section "Problems with Scheme" in the motivation doc and got a similar impression. The last three short paragraphs were reasonable on why not Scheme for this, but they were preceded by a greater bulk of confused or vague complaints. (E.g. "nil being mixed with '()" -- what nil?)

> like transcriptions of vibes derived from AI discussion

I was wondering whether a human wrote it too.

Quite possible this section was unrepresentative! I hope so.

[Joker_vD]

Also, a rather weird hostility toward type aliases (as opposed to newtypes). Almost nobody really uses "type A = int" in Go except for abbreviating the imported types which AIUI is its main purpose; that's why it is slightly longer and harder to type than the newtype declaration "type A int".

And frankly, if your main goal is to prevent RCE exploits... start by splitting the call stack and the data stack, you don't even need to invent a new language for that; a C implementation doing so is perfectly in its right. Adding boundary checks on array/pointer accesses to C would indeed be harder — but we already have Ada for that.

[bOZbfU4YdRnJQ]

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-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.

[mccoyb]

I agree with you that my original message was sloppy, and also with your claim that full Rust has not been mechanically proven sound.

But that is not the same claim as “safe Rust can cause UB"

If you are claiming the latter, please provide a minimal safe Rust program that causes UB without unsafe, FFI, proc-macro tricks, compiler bugs, or an unsound safe API implemented using unsafe?

If you can produce such a program, of course you are right.