upvote
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