6 ms·
> In contrast, the Rust type system has been mathematically proven to be correct. Is this the case? E.g. the issue "Prove the Rust type system sound" https://g
by _flux 2y ago
> In contrast, the Rust type system has been mathematically proven to be correct.
Is this the case? E.g. the issue "Prove the Rust type system sound" https://github.com/rust-lang/rust/issues/9883 https://github.com/rust-lang/rust/issues/9883 is closed with comment "This will be an open issue forever. Closing." in 2016: https://github.com/rust-lang/rust/issues/9883#issuecomment-242452073 https://github.com/rust-lang/rust/issues/9883#issuecomment-2... .
At least nowadays (since 2022) we do have a language specification for Rust: https://ferrous-systems.com/blog/the-ferrocene-language-specification-is-here/ https://ferrous-systems.com/blog/the-ferrocene-language-spec...
- aw1621107 2y agoThe closest thing is probably RustBelt [0], which proved the soundness of a subset of Rust that included borrowing/lifetimes. This was later extended to include relaxed memory accesses [1]. Neither of these papers include the trait system, unfortunately, and I'm not aware of another line of research that does (yet?). [0]: https://dl.acm.org/doi/10.1145/3158154 https://dl.acm.org/doi/10.1145/3158154 [1]: https://plv.mpi-sws.org/rustbelt/rbrlx/paper.pdf https://plv.mpi-sws.org/rustbelt/rbrlx/paper.pdf