4 ms·
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, b
by _flux 2y ago
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.
- Measter 2y agoYou might be thinking of CVE-RS[0] which is exploiting bugs in the compiler. [0] https://github.com/Speykious/cve-rs https://github.com/Speykious/cve-rs
- _flux 2y agoYou 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.
- steveklabnik 2y agoJust one. It’s a compiler bug and not a soundness hole.
- _flux 2y agoI 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 https://github.com/rust-lang/rust/issues/9883 Per https://blog.rust-lang.org/2023/01/20/types-announcement.html 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.