News for hackers. Stuff that matters.
Re:Smart pointers for the kernel by lertn on Friday October 18, 2024 @05:53AM (#41877802)
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.

Re:Smart pointers for the kernel by Measter on Friday October 18, 2024 @07:44AM (#41878455)
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