I'd like to see the Ada guys, and especially the SPARK guys, talk about Rust the way Rust people talk about C. That said, I'm just gonna add ACL2 to my Common Lisp toolbox and then I too will have the power of theorem proving.