4 ms·
It would be cool if the unsafe aspects of Rust that are necessary (like Vec) could themselves be formally verified, like when each edition of the language gets
by asimpletune 4y ago
It would be cool if the unsafe aspects of Rust that are necessary (like Vec) could themselves be formally verified, like when each edition of the language gets compiled or something. I know some languages include proof tools but they're not super popular, and Rust's compiler helps a lot. Still, it would be really cool to know, or at least know that you can't know. LinkedList is another example. There's no way to really write a linked list in the rust friendly way, so you have to use some boxing. All of that is fine, it probably works, but what if I forgot later, and changed something about the implementation, introducing bugs around edge cases or what not.
- Jweb_Guru 4y agoThis process is actually already underway, notably with the RustBelt project: https://plv.mpi-sws.org/rustbelt/ https://plv.mpi-sws.org/rustbelt/. It has not yet achieved the kind of tight integration with the source language that stuff like Creusot has, but everyone would like it to move in that direction :) For the specific case of Vec (and a few other types--e.g. Cell, Mutex, etc.), as I mentioned, a recent paper by xavxav actually proves that the important parts of the unsafe implementation of Vec do actually fulfill the signatures that are used by the CreuSAT proof. This is part of https://people.mpi-sws.org/~dreyer/papers/rusthornbelt/paper.pdf https://people.mpi-sws.org/~dreyer/papers/rusthornbelt/paper..., which I believe won the distinguished paper award at this year's PLDI!