Hacker News Reader

Comment by GrantMoyer | Hacker News Reader

It's surprising this bug went unnoticed for so long, but at least it's easy to fix, since it's not a bug with the type system itself; it's just a bug in the compiler. The compiler should always have been rejecting that code according to lifetime rules of Rust's type system, so the fix is to just make it reject the code, rather than having to change the fundamental rules of lifetimes.

View on HN

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.

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

Rust scores a lot higher on the safe scale than Python scores on the fast scale. Also, who are these mythical people that call Python fast?

Python calls itself fast in its own webpage:

https://www.python.org/about/

  Python is powerful... and fast; plays well with others; runs everywhere; is friendly & easy to learn; is Open.

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?

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?

You can't formally verify the soundness of something that inherently necessarily relies on hardware implementations that themselves could be faulty.

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

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)

Just run it on open hardware.

Note that the Lean kernel itself is not formally verified.

Don't let the OpenAI marketing department hear you...

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.

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

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

Not knowing anything about rust, the problem in these type of case is making it rejecting that bad code without also rejecting valid programs. But maybe this is indeed easy to fix, I don't know.

There are no such valid programs. Proof by contradiction:

A valid program would be exploiting undefined behavior in rust, but rust has no undefined behavior. Thus such a program must not exist.

Now a program may appear to work before the fix, but it was never a valid Rust program.

I can't tell if you are sarcastic, but in case you are not:

By Rice's theorem you cannot be sound and complete, i.e. accept all valid programs and reject all invalid ones. Most languages choose to be sound but not complete, i.e. reject all invalid programs but also some valid ones (C and C++ are the notable exception, although most languages have escape hatches). GP was saying that the fix might reject valid programs that compile today. This is true for some existing soundness bugs, but not necessarily for this one specifically.

Rice's theorem does not apply. This is not about what the compiler does, it is your program. If your program is not sound then it is invalid Rust even if the compiler accepts it and it seems to do the right thing.

That said, I was sarcastic.

It does apply, of course (even if not to this case specifically). The implemented Rust semantics are not sound, as evidenced by this issue. We need to find (or adjust) sound semantics. Which, mathematically, is equivalent to designing Rust from scratch (ignoring things like RustBelt because they did not formalize the entire system). Due to Rice's theorem we know we need to give up some sound programs. Can we give up exactly the programs we already gave up for the previous Rust? Maybe, maybe not.

> The implemented Rust semantics are not sound, as evidenced by this issue. We need to find (or adjust) sound semantics.

You’re ignoring the possibility that Rust semantics are sound, and the implementation doesn’t fully implement them. In that case, we do not have to find sound semantics.

That, I think, by far is the most likely option.

Reason: I’ve not seen a single comment claiming the example should compile, and zillions (implicitly) acknowledging this is not what Rust should do.

I explicitly did not ignore the option that there are possible sound semantics:

> but not necessarily for this one specifically

> Maybe, maybe not.

But "the Rust semantics" are not defined, formally. The closest we have is what Rust implements currently, and that was shown here to not be sound. Other than that, we maybe have vague ideas in the brains of some T-types members, which are not detailed enough to determine soundness (source: those type system people want to formalize the semantics so they will be).

And for the record, we know of other soundness issues where the likely resolution path will involve rejecting valid programs we accept now, and the only question is how many.

"the Rust semantics" are defined informally as sound. Anything that the implementation accepts that is unsound is a bug. We might never be able to prove the rust implementation, and may forever find loop holes, but informally it is sound and that is the intent.

There is no such thing as "informally sound". Soundness is a mathematical property and needs to be proven mathematically. For that, you first need a mathematical definition.

The tricky thing about formalization is that you usually have to reimplement the type checker into a proof assistant in order to do formal soundness proofs. It's not necessarily clear that this reimplementation is identical to the actual Rust compiler (in fact, you often have to massively simplify the type system to make the proofs tractable), so bugs in implementation can cause unsoundness without being related to fundamental flaws in the soundness of the type system.

Indeed. Proving the implementation will likely never be done, it's just way too hard. But proving Rust abstract semantics are sound will by itself be a major leap forward (RustBelt did that for a subset of Rust).

It could be that I'm totally yapping bullshit, but the "designing from scratch" can vary depending which field of maths you're talking about. For instance, if we model the semantics as a series of composable functions, then you only have to scratch only the specific dependency tree of the functions. Basically everything can be reused with no wasted work, and the output space gets culled.

Which is why I said to ignore RustBelt. Because we don't have formal semantics today, we only have the actual implementation which is not composable.

Terminological nitpick, but soundness is a property of an entire type system not of an individual program. A type system is sound if it only accepts valid programs. A program is valid if it never exhibits undefined behavior.

Rice's theorem implies that it's impossible to precisely distinguish valid and invalid programs just by looking at their source code. Thus Rust rejects some valid programs in order to be sound (e.g. "if false { None.unwrap_unchecked() }").

In the case of the bug report in OP, I don't think that there are many valid programs in practice that exploit this soundness issue, so fixing it just means rejecting more invalid programs.

Rust does not target Turing machines so Rice's theorem does not apply.

Rust does have undefined behavior, though.

In this case the issue is that the compiler just isn't properly type checking the implicit call to the drop method that's inserted at the end of the nested block. AFAIK, no correct code should depend on the absence of that check.

Reply on news.ycombinator.com