4 ms·
> an implementation of it that uses unsafe, like the one in crossbeam-rs, is typically very amenable to theorem provers (much more than C) Just wondering, how
by pca006132 5y ago
> an implementation of it that uses unsafe, like the one in crossbeam-rs, is typically very amenable to theorem provers (much more than C)
Just wondering, how many unsafe code in commonly used libraries (standard library, tokio etc.) are proved using theorem provers?
- volta83 5y agoMost of the unsafe code in libcore is proved in Iris. Some of the unsafe code in the standard library also. Some parts of crossbeam have pencil&paper proofs documented.
- steveklabnik 5y agoDon't have comprehensive enough data to know, but part of the standard library was proven via the Rustbelt project, and it found some places where there were bugs, as well as some places where things could safely be loosened up.