Hacker News new | past | comments | ask | show | jobs | submit login
RustBelt: Computer Scientist proves safety claims of Rust programming language (eurekalert.org)
28 points by lsllc 6 months ago | hide | past | favorite | 2 comments



He only proves type safety, and layed out ways to prove special type safeties even in type-unsafe code.

He didn't tackle the two other rust unsafeties, memory and concurrency.


> RustBelt is a formal model of Rust’s type system, together with a soundness proof establishing memory and thread safety. [1]

[1] https://people.mpi-sws.org/~jung/thesis.html




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

Search: