[Rusky]

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]

> 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

[simonask]

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]

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.

[_flux]

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.

[Measter]

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

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

[_flux]

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]

Just one. It’s a compiler bug and not a soundness hole.

[johnisgood]

That code looks horrendous.

[lertn]

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]

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