Yeah, me too. However, I think we should wait for the formal verification of Rust to be completed before trying this. While it is possible to make something SPARKish without complete formal verification, it's probably better to build it using concepts learned during the formal verification.