This Dafny thing seems absolutely cool. I didn't check the details but a 30 seconds read tells me that if it could generate rust code (it can Java, C, so it's not unbelievable), then we're in for a better world !