This got me intrigued. Is there a soundness proof for the Rust type system? The ... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		lertn on Oct 18, 2024 \| parent \| context \| favorite \| on: Smart pointers for the kernel 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 on Oct 18, 2024 [–]

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

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact