upvote
There never was formal verification of the entire rust compiler, or even its complete borrow checker/type system. There has been verifications on _subsets_ of them.

Also, a lot of those soundness issues aren't related to new features _at all_, but usually due to poor assumptions made in optimizations.

The soundness bugs _are_ taken seriously though, and are slowly being patched out. A lot of the links in OP are now closed because Rust either changed how it generates code to avoid the issues, or fixed LLVM.

reply
not of the implementation. Of the type system. And a verification of subsets, but not a verification of their interactions == the whole system is unverified.
reply
The eventual goal is verification of the full system. Not the implementation, yes, that's infeasible. But this will mean all soundness bugs will be either found and fixed or we'll know how to fix them once they're found. In any way they won't be fundamental (which is believed to be the case today, but not proven).
reply
so why put them in before knowing if they work reliably? That's the YOLO part, to me
reply
The same combination of reasons we've been doing these kinds of heuristic implementations forever:

- people still get value off of an incomplete implementation, because we are allowed to be mindful of the issues (see, eg, UB in C++). In other words, many, many more bugs have been prevented by the borrow checker working as intended than have been caused by it working poorly. It's not particularly close.

- theory almost always moves slower than practice

The mutable state situation pointed out by the grandparent poster was a famous issue in typing SML under mutability that required serious changes in the language, see Section 4.2 here: https://smlfamily.github.io/history/SML-history.pdf

These were Turing-award caliber people figuring it out and, according to your definition, "yolo"ed it. This stuff is _hard_, and these driveby comments truly aren't helpful.

reply
Because there’s real value delivered even before that? Perfect bring the enemy of good and all that
reply
You're claiming that this bug that reproduces back to Rust 1.4 (2015) is a sign they're adding too many features to make sure they don't introduce bugs? Or do you have bugs that are due to these recent features?
reply
It holds that ¬(∀subsets: isverified(subset)) but it's not true that ∀subsets: ¬isverified(subset), which it think most people would interpret "the whole system is unverified" as
reply
If I independently verify that subsystem A properly consumes apples, and that subsystem B is properly emitting oranges, but never verify that subsystem A is receiving apples, and just connect subsystem B to it, then yeah, the system is not verified.
reply
That's not the issue though.
reply
you’re deeply confused but the words “validation” and “qualification” may help untangle the web, there’s a lot more to assurance than what your model seems to hold (and you’re drawing batshit deductions from it)
reply
No mainstream compiler is formally proven. If you want a verified compiler, you pretty much have to choose between using a subset of standardml or a subset of C and the one proven compiler for each.
reply
You're mistaking the semantics of the type system, from the implementation. I'm not talking about verifying the compiler. There's nothing to verify there.... literally. There is no spec to the language. By definition it is verified because the only verification you can do is tautological: "does this rust compiler do what this rust compiler does?"

But the unsoundness is because the type system itself, abstractly, was not verified. Or the interactions between parts. I.e. If you verified the compiler you'll find that it implements the algorithms perfectly. But tells you nothing about whether those implemented algorithms, however perfectly implemented, actually provided those guarantees.

reply
They probably meant things like LLVM and the various optimization passes. None of those are verified, there’s probably all sorts of correctness issues, and yet it’s still ok. Rust’s usage also has issues and bugs emitting the right intermediate form for LLVM to consume and usually also it’s ok.

Would it be nice if we had even higher level of quality? Yes. But what’s neat is we have empirical evidence - Rust code does achieve the memory safety goals over C++ even though there’s bugs in the compiler. That’s why Rust is very quickly eating all things C and C++. A huge amount of value that the industry would just be unable to access for a long time if you waited for everything to be formally proven.

reply
Okay, but verifying a type system and language specification for soundness wouldn't actually give you any of the guarantees you want if the compiler toolchain isn't verified to implement them correctly. And this sort of thing just isn't standard practice in the industry and never has been. Sure it would be nice if more things were verified, and we are somewhat headed in that direction, but it seems weird to say that rust specifically is just a bunch of half-baked yoloing because it doesn't do something that essentially no other language is doing either.
reply
Wait, there's a proven subset of C? Can you point me to some info?
reply
There is a massive possibility space between “yolo” and formal proof. Rust has substantial evidence of correctness. For example, unit tests and types.
reply
That's verifying the implementation. The type system wasn't verified. It implements stuff perfectly, it has tests that prove it, but nobody formally verified that they perfectly implemented the correct algorithms
reply
Tests are not perfect, but they are a lot better than where we were in 1990.
reply
completely tangential to whether you're testing for the right thing.
reply
We are a lot closer to testing the right thing today than we were in 1990!

There are pros and cons to tests, but they do some things very well. For starters a test is a lot better sign that things work as intended than a formal proof which is often so abstract most people can't be sure how it relates to what was intended. You can prove something correct that is clearly wrong. While a test will only test the one case, at least it is typically easy to understand that case and why that answer is correct. Of course if your requirements are correct your proof will tell you it is correct for all cases while a test is limited to that one case. Again pros and cons, and people speaking against tests are not honest about those.

reply
[flagged]
reply
I think the difference is here:

- If a compiled C++ program has unsound behavior, the program needs to be fixed

- If a compiled safe Rust program has unsound behavior, the compiler needs to be fixed

reply
> - If a compiled safe Rust program has unsound behavior, the compiler needs to be fixed

Not really: the program still needs to be fixed, but fixing the compiler ensures that this unsound behavior never happens again to anyone. So you have two bugs to solve (vs C++'s one bug) but then you kill an entire class of unsoundness bugs just by recompiling.

reply
That's not completely correct. If the Rust or C++ compiler has a bug in both cases either the compiler has to be fixed or the program can be adjusted to work around said compiler bug If possible. However, It's fair to argue that the Rust compiler makes more assertions and is more complex, which results in a larger error surface.
reply
Which is better, surely? One fix for every program written in Rust vs everyone having to fix it themselves…
reply
> If a compiled safe Rust program has unsound behavior, the compiler needs to be fixed

Can you provide an example of such a program that can’t be fixed at the program level like a C++ example?

reply
Sure, usually the program can be changed to avoid the issue, but the key here is that the Rust compiler is wrong and needs to be fixed. Once fixed, the actual program fix also falls in place, as it cannot be compiled anymore.
reply
That's the same kind of issue like a bug in a C++ compiler.
reply
The average cause of unsoundness in a C++ program is not a C++ compiler bug
reply
This is about an issue in the type checker, which would lead to unsoundness also in a C++ program. And also in Rust most causes of runtime failures are actually things that happen in `unsafe` blocks.
reply
> You can be annoyed by Rust fanboys, sure, but the more annoying are the Rust haters, because the hate always comes from a place of ignorance.

For what it's worth, Rust fanboys also seem just as vulnerable to their ignorance of C/C++ compiler extensions and tooling (e.g. sanitizers, bounds annotations, standard library hardening modes and so on.) which are just normal part of professional C/C++ use today.

reply
And are also woefully insufficient as proven in most sanitized & linted & fuzz-tested programs in existence (browsers and operating systems).
reply
Compared to what? CVE-2025-68260?
reply
Compared to, for example, 5 million Rust lines in Android, I'd say.
reply
Yeah, the anti-Rust crowd seems to just hate Rust and completely ignore all the empirical evidence that professional C++, even using all the TSAN, ASAN etc still has ~10-100x the memory safety issues of Rust without any of that. I think they think “oh - use after free and out of bounds are trivial to solve” and ignore the enormously meaningful order of magnitude harder thread safety. Not to mention that sanitizers are only effective at validating the code paths exercised within the test suite. Production manages to test all the things your test suite missed. The Rust compiler verifies stricter properties about your program proof being correct in all cases (within the bounds of its own correctness of course, but that’s higher than all other code combined).
reply
> “oh - use after free and out of bounds are trivial to solve” and ignore the enormously meaningful order of magnitude harder thread safety

This is what advocates of Rust are guilty of and CVE-2025-68260 is an example of it. Ultimately TSAN and KTSAN exist for a reason, and rust devs should learn how to use them effectively.

reply
I'm not saying don't use sanitizers. I'm saying that even without sanitizers you're better. Also, this CVE isn't strictly a Rust problem - it's a problem creating safe boundaries around unsafe C code which was difficult even for the Rust standard library to suss out and even harder in kernel land where the rules are often not even documented. It'll take time but I don't see how this is an inditement. I can point to the myriad of CVEs the kernel has in C code regardless of sanitizers being used - what consistent and equal standard are you upholding those lines of code to.
reply
Formal verification of the type system does seem a worthwhile goal, and to my understanding it's something the community has been making progress towards, but I also understand it's still relatively uncommon for most languages.

Is this more an abstract concern over the state of the industry, or is there a specific language you had in mind that you'd prefer Rust was modeled after?

reply
Relatively uncommon as in there is not, as far as I know, a single mainstream language with a formally verified spec.
reply
Important to note that this is is not a bug in the type system itself, it's a bug in the borrow checker not enforcing invariants that the type system says that it should, and formal verification of the type system would not have helped here.
reply
The Java type system is also unsound. That’s life. It is hard to do this fully correctly. In practice this never comes up.
reply
While true, there are two important differences:

1) Unsoundnesses in Java's type system are checked at runtime.

2) They (or at least some) are intentional or at least won't-fix bugs.

Both are not true for Rust.

reply
The font color is so close to the background now that I can't even read your edit. Sorry, bud.
reply
As you can see, this is a true statement, but HN really really really hates it for some reason.
reply
Yes. When people describe Rust as "a memory-safe programming language" they are describing an aspirational vision, and not a programming language that has actually been designed with sufficient rigor to guarantee memory safety. Any failure of rustc to actually guarantee this is just a bug in rustc itself, a failure to properly implement the Rust spec, because the closest thing Rust has to a spec is literally just the vague ideal that the compiler should guarantee safety somehow.

Rust cannot fail, it can only be failed.

reply
I don't think the definition of "memory safe" has ever required full end to end stack conformance with a proof. Very few languages have achieved that, though some have. Most people call Java memory safe, C#, Python, Typescript, etc - all of those fall short of a formally verified, sound type system with a verified toolchain.
reply
Not to talk about Go, which has intentional unchecked-at-runtime UB (data races) yet many argue to consider it memory safe (and I have a feeling that the same people arguing Rust isn't memory safe are also there. Just a feeling though).
reply
deleted
reply
deleted
reply
> Rust cannot fail, it can only be failed.

“Please build the perfect system. Because I specified ‘perfect’ any flaws are due to your incomplete implementation, not my awful brief.”

If the person writing the rust spec was a client I would have to drop them because they would be setting themselves up for dissatisfaction.

reply
Would you say the same thing about Java? It’s type system is also unsound.
reply
I'm not an expert on the Java specification, but my understanding is that Java as a language is well-defined enough that we can say things like "Java's type system is unsound", independently from any specific implementation of Java.

You can't do that with Rust because "Rust's type system" is literally just the vague concept of "a type system that is safe". The implementation of this ideal in rustc can have flaws, but Rust itself cannot, because Rust itself has no flaws by definition.

reply
It is true that Rust does not have a complete formal specification for its type system which has been analyzed and proven to be sound.

You seem to be implying that because of this, Rust has no definition of its type system (other than whatever happens to be implemented in the current compiler). I would disagree.

As evidence, I would like to point out that not a single person argued that this flaw was not a bug, but was in fact the officially defined behavior. Clearly, the community has a shared understanding of what Rust's type system "ought" to do.

reply
The true specification was inside our hearts all along!
reply
I mean yes, part of our understanding of systems is a social one!
reply
Sure, but in Rust's case the social understanding is "there exists some type system that guarantees perfect memory safety, and has the general aesthetic features associated with rustc's type system, and 'Rust' is defined to be whatever that type system ends up being".

This is a nice ideal, but it doesn't actually exist in concrete terms as a design. It can never have flaws because the definition of it is just "rustc without all the flaws".

reply
Haskell is in a similar boat with regards to a missing formal spec.
reply
but it isn't claiming to be saving you from things it can't prove it can either.
reply
Memory safety was always a major selling point for java.
reply
>Rust cannot fail, it can only be failed...

Sweet. But why should anyone care..

reply