I'd like both. SPARK's stuff was ported to Ada 2012. It can be done for Rust as well. The trick is to make it optional so people don't have to pay attention to it. Maybe even have editors filter it out for people not paying attention to it. At the least, it being used in standard library and OS API's would let it enforce correct usage of those in debug/testing mode. 80/20 rule says that should have some impact given how much damage we've seen C and Java developers do misusing the foundational stuff.
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.
