6 ms·
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
by 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 agoThere 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