[hannesm]

This is similar to my experience verifying imperative code (as part of http://itu.dk/research/tomeso): rewrite code as pure as possible (learning that mutation is premature optimisation), then try to specify and prove it.

Aside, if we're reinventing the wheel anyways, why not in a proper style? There's no reason to not deploy purely functional code (+some effectful shims). Think https://mirage.io https://nqsb.io -- rust has way too much mutation and unsafe builtin already...