Comment by WiSaGaN
11 days ago
It's fascinating that this kind of bug is exactly you can't really avoid even when rust is supposedly to guard against. Rust mitigated this problem a lot in practice, but you can never be certain because of issues like this in practice. This is similar that a math proof that's already been peer reviewed and accepted as truth, may still be possible to be wrong, although the chance is very small but it's not zero. Epseicially when the complexity gets higher.
> It's fascinating that this kind of bug is exactly you can't really avoid even when rust is supposedly to guard against.
Note that Rust is not a theorem prover and Rust programs are usually not formally verified (there are some extensions like Creusot to verify Rust programs, but they are incomplete and a work in progress)
Compiler bugs are, like, just logic bugs. There's a project to eliminate compiler bugs that cause unsoundness, project zero [0] but, still, without formally verifying the implementation, there is nothing really guaranteeing there's no such bugs left.
(note: unsoundness in this context means having safe code cause UB due to a compiler bug; the fix is usually to make the compiler reject the code with a compiler error)
To make matters worse, Rust still doesn't have a spec, and there is not even a tight definition of what are the rules of unsafe code - that is, what rules you must follow so that you unsafe code doesn't trigger UB. Discussions around this are done mainly in issues of the unsafe code guidelines repo [1]
[0] https://goals.rust-lang.org/2026/roadmap-project-zero.html
https://github.com/rust-lang/unsafe-code-guidelines/issues
> Note that Rust is not a theorem prover
Not that that would make any difference, theorem provers can also have bugs. Famously this summer someone “disproved” the collatz conjecture by exploiting a soundness bug in Lean.
How is this different from any other compiler bug?
There was one in the Linux kernel a while ago that mistakenly eliminated an important null check.
Is this different?
No, people who don't actually use Rust just like to pretend it's something more than it is, for some performative outrage or something.
Here's the current list of similar (unsoundness-causing) open compiler bugs in Rust:
https://github.com/rust-lang/rust/issues?q=state%3Aopen%20la...
Oh, I think you're so right. I heard ton of people online assuming that Rust could help to catch any freaking bug, and when they noticed that - well, it obviously doesn't - ah, then it's just crap or hype.
In theory it would be possible to formally verify the soundness of the borrow checker. Maybe with AI advances we'll be able to do that in the near future. I mean, how much more complicated can it really be than proving Navier-Stokes?
Note that the Lean kernel itself is not formally verified.
Don't let the OpenAI marketing department hear you...
You can't formally verify the soundness of something that inherently necessarily relies on hardware implementations that themselves could be faulty.
You take hardware properties as axioms (for instance, ARMv6 cache coherency is specified in detail as part of the lengthy spec, even though you have no guarantees that the hardware actually is faithful to the spec)
You can certainly verify the soundness of what is within your control, the compiler code, which is what is being suggested above.
You can formally verify that the algorithm has the desired properties, though. If the hardware requires additional properties for soundness, then that would only be an error in the properties, not in the proof. (Of course, that would no longer prove soundness on that hardware.)
Just run it on open hardware.
Interesting, the main argument is that C need too much expertise of programmer to avoid problems.
Now, you have a language sold as safe, with popularity made manily blaming C... but now we can say it gave the false sense of safety, distracting programmers from real issues in the name of its error messages that lead for endless refactoring if some new feature is added to project just to o have peace with the compiler. It is a language that program the programmer, an inversion of roles.
No, this isn’t the way to interpret this. Rust has been very successful not just in appearing safer, but actually delivering safety over C. The sense of safety was almost entirely real. Just some situations it didn’t cover.
I don't understand why people talk about this like we live in some fantasy land where C compilers don't have tons of bugs like this. And that's just the bugs, not even the accepted UB.
4 replies →
> but now we can say it gave the false sense of safety
Except we can't say that, at all. This is just a single bug in relatively obscure code, so 99.99999% of your code remains safe.
Meanwhile in C, 100% of your code has the potential to trigger a similar bug, except there's no path for the underlying cause to ever be fixed, unlike here.
You're essentially complaining that something isn't 100% safe, but that's just your misconception of what "safe" means. Nothing is 100% safe, not can it ever be.
It's especially ridiculous to then compare something 99.999% safe to something 0% safe and conclude that all that "supposed safety" is useless, because look: in 0.001% of cases it's NOT safe!
Both the "100% of of your code has the potential to trigger a similar bug" and "there's no path for the underlying cause to ever be fixed" are just nonsense.
Imperfection isn’t evidence of ineffectiveness.
Considering this has gone unflagged for 11 years... Finding a flaw in Rust’s safety guarantees doesn’t mean that they provide no benefit, over a programming language without them.
>but now we can say it gave the false sense of safety
Ok, but that perspective is only valid from Rust++ users who get to mog both Rust and C users. It's not a valid perspective from C users.
Also, your position against Rust is really strange to me, because I love the lack of mutable aliasing. If you think it is a punishment for the programmer you're stuck in a programming model from the 70s. Rust's model is theoretically optimal both from a hardware design perspective and a compiler perspective.
VLIW compilers love Rust because the lack of mutable aliasing by default allows aggressive instruction reordering and instruction level parallelism! Software managed caches are only possible by essentially dragging the cache coherency protocol into the software level!
The sad news is that LLVM is a classic compiler backend optimized for mutable aliasing, which means it is not that great at producing code for VLIW architectures.
... and even if you formalize it, it could still be false due to an error in the theorem prover itself.
And even if the theorem prover has no errors, the math behind the theorem prover could be inconsistent according to Gödel's incompleteness theorem. So even in principle, we can never be completely certain about the soundness of Rust, though the more theoretical concerns tend to be dwarfed by basic human error.
I think it's a good thing to keep in mind, that the actual implementation of Rust almost certainly isn't sound. Even an "ideal Rust" still has unsafe, which can affect the soundness of even faraway safe code. But I don't think it's nessesarily wrong to talk about Rust as if it were safe. Much of our communication has implicit assumptions, and the way we talk about Rust is no different. It would be exhausting to qualify every discussion of saftey with "assuming the compiler has no bugs", "assuming all unsafe code follows the (not fully specified!) rules", etc.
Ultimately it's like any other implementation of theory into practice. The theoretical model of Rust lets us reason about and design an implementation to achieve certain practical goals even though the model is a simplification of reality. In Rust's case, practical use has demonstrated it achieves design goals like reducing bugs and reducing development time (compared to peers like C++) to a substantial degree.
It’s like Python describing itself as fast. Everyone knows that means “fast enough for intended use”, not “fast in an absolute sense”. But for some reason when Rust describes itself as safe people take that to mean in an absolute sense.
2 replies →
Gödel and halting problem don't apply to real programs, because they don't need to be accurate: they can reject correct code.
Or more likely, an error in the formalization. "What you proved is true, but it's not sufficient for what you care about." See for example WPA2 KRACK attacks after WPA2 was proven secure.
This moving of goal posts whenever correctness through type systems is being discussed is a bit tiresome, because it quickly leads to such ad absurdum corner cases.
Yes, you are all correct. The compiler may have a bug. And if it does not, then the type system may have a problem. And if it is formally verified, then the theorem prover might have issues. And if it does not, then the very math it relies on may be wrong.
But what do we contrast this to, what is the alternative to correctness through the type system? Almost every time, when it isn't "nothing", it's "tests". We rely on tests to test whether the program behaves correctly.
And as we all know, quite in contrast to type systems and their checkers, tests are always error-free, complete, and sensible?