If you keep unsafe code in modules and don't pass raw pointers in between, it is much easier to audit the code. All the glue code is automatically safe. Then ea

If you keep unsafe code in modules and don't pass raw pointers in between, it is much easier to audit the code. All the glue code is automatically safe. Then each module can be audited separately to make sure it is impossible to make it crash by using public API. Rust `collections' library is full of unsafe code. Just for example: https://doc.rust-lang.org/src/collections/up/src/libcollections/btree/map.rs.html https://doc.rust-lang.org/src/collections/up/src/libcollecti... But you can never leave a BTree in an invalid state by adding or removing elements. Given safe collections library you can write lots of applications without resorting to unsafe code and having to prove the safety of your code. Proving safety of B-Trees, threaded code and things like that requires a whole theorem prover that Rust most likely will never provide. You need to use Coq or similar tool if you are developing new algorithms and data structures. But if you are not a pure computer science researcher, most likely you don't need it. All you have to do is to carefully translate pseudocode from paper into Rust and package it.