"Ada died off. " On the verification side, it's never had more users that I'm aware of. SPARK and Frama-C are very active compared to almost non-existent use o

"Ada died off. " On the verification side, it's never had more users that I'm aware of. SPARK and Frama-C are very active compared to almost non-existent use of formal methods in industry decades ago. Rust could similarly have a subset integrated with Why3 platform to make the formal methods easier to use. Further, I've seen extraction done from Coq to C and Rust. There's also one person modeling C in WhyML to write the algorithms in the latter but extract to former. Or something like that. Could be done for Rust, too.