[steveklabnik]

I hear you! As I said, these things take time.

The interior mutability primitives in the standard library already have a proof, incidentally. Look at the Rust Belt work.