Hacker News new | ask | show | jobs
by im3w1l 606 days ago
> In Rust, because the type system is sound

Unfortunately, it's not. Now I do think it will be eventually fixed, but given how long it has taken it must be thorny. https://github.com/rust-lang/rust/issues/25860

2 comments

In practice this is a compiler bug, though, and is treated as such, and not a soundness hole in the abstract design of the type system.

There has also not been a single case of this bug being triggered in the wild by accident.

I take this to mean e.g. the Oxide project has proven the Rust type system sound?

There was a Git repository demontrating unsoundness issues in the compiler, but I seem to be unable to find it anymore :/. It seemed like there would be more than one underlying issue, but I can't really remember that.

I tried to look into it, and it does not seem like the type system is proven, yet, though the issue itself is closed: https://github.com/rust-lang/rust/issues/9883

Per https://blog.rust-lang.org/2023/01/20/types-announcement.htm... there is a roadmap for ensuring Rust type system soundness end of year 2027. I think it means the implementation.

You might be thinking of CVE-RS[0] which is exploiting bugs in the compiler.

[0] https://github.com/Speykious/cve-rs

You are quite likely correct. My search term included "unsound", and it missed this one.

But this time I've starred and cloned it!

I didn't quite see if this actually exploits multiple bugs or leverages just one, though.

Just one. It’s a compiler bug and not a soundness hole.
That code looks horrendous.