undefined

points

[-]

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.

by afdbcreid10 hours ago|

parent|

[-]

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.

by bluGill8 hours ago|

parent|

[-]

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.

by i2talics6 hours ago|

parent|

[-]

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.

by afdbcreid7 hours ago|

parent|

prev|

[-]

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.

by i2talics6 hours ago|

parent|

[-]

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.

by afdbcreid6 hours ago|

parent|

[-]

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

by Someone6 hours ago|

parent|

prev|

[-]

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

by afdbcreid6 hours ago|

parent|

[-]

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.

by Permik6 hours ago|

parent|

prev|

[-]

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.

by afdbcreid6 hours ago|

parent|

[-]

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.

by charcircuit8 hours ago|

parent|

prev|

[-]

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

by wging4 hours ago|

parent|

prev|

[-]

Rust does have undefined behavior, though.

by foldr9 hours ago|

prev|

[-]

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.