3 ms·
I am surprised they didn't mention Iris[1] and RustBelt[2] projects. Iris works on creating the formalization framework based on separation logic and Coq. They
by xvilka 7y ago
I am surprised they didn't mention Iris[1] and RustBelt[2] projects. Iris works on creating the formalization framework based on separation logic and Coq. They have the Rust code model specifically[3].
[1] https://iris-project.org/ https://iris-project.org/
[2] https://plv.mpi-sws.org/rustbelt/ https://plv.mpi-sws.org/rustbelt/
[3] https://gitlab.mpi-sws.org/iris/lambda-rust https://gitlab.mpi-sws.org/iris/lambda-rust
- Argorak 7y agoThis is mainly a lapse. Thanks for highlighting them, they do awesome work! They are also not quite what Sealed Rust is about. RustBelt is about formally verifying Rust and improving the understanding of the language. Sealed Rust is mainly about the industrial adoption process. It's not meant as a replacement or competing project, quite the contrary: RustBelt existing is a huge motivator and a major stepping stone to build on. We are also personally in touch through the Rust project.