6 ms·

It's not the same unwritten social contract: in Rust even the unsafe code has the same stricter type signatures as the safe code, so there is a formal way to ju

by Rusky 2y ago

It's not the same unwritten social contract: in Rust even the unsafe code has the same stricter type signatures as the safe code, so there is a formal way to judge which part of the program is at fault when the contract is broken. You might say the contract is now written. :-) In C, the type system does not express things like pointer validity, so you have to consider the system as a whole every time something goes wrong. In Rust, because the type system is sound, you can consider each part of the program in isolation, and know that the type system will prevent their composition from introducing any memory safety problems. This has major implications in the other direction as well: soundness means that unsafe code can be given a type signature that prevents its clients from using it incorrectly. This means the set of things the compiler can verify can be extended by libraries. The actual practice of writing memory-safe C vs memory-safe Rust is qualitatively different.

im3w1l 2y 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 https://github.com/rust-lang/rust/issues/25860
- simonask 2y ago
  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.
  - _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 ago
      You 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 ago
        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.
        steveklabnik 2y ago
        Just one. It’s a compiler bug and not a soundness hole.
    - _flux 2y ago
      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 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.
- johnisgood 2y ago
  That code looks horrendous.
lertn 2y ago
This got me intrigued. Is there a soundness proof for the Rust type system? The only language with such a proof that I am aware of is StandardML. Even OCaml is too complex for a soundness proof.
- Measter 2y ago
  There was a paper a few years ago[0] was related to proving soundness. That could be what they meant. [0] https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf

by Rusky 2y ago

im3w1l 2y 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 https://github.com/rust-lang/rust/issues/25860

simonask 2y ago
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.
- _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 ago
    You 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 ago
      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.
      - steveklabnik 2y ago
        Just one. It’s a compiler bug and not a soundness hole.
  - _flux 2y ago
    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 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.
johnisgood 2y ago
That code looks horrendous.

lertn 2y ago

This got me intrigued. Is there a soundness proof for the Rust type system? The only language with such a proof that I am aware of is StandardML. Even OCaml is too complex for a soundness proof.

Measter 2y ago
There was a paper a few years ago[0] was related to proving soundness. That could be what they meant. [0] https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf