3 ms·
Rust is not yet ready for formal verification, along with some ready libraries for that purpose, unlike Ada/SPARK. Hopefully, it will be there, just not yet. It
by xvilka 5y ago
Rust is not yet ready for formal verification, along with some ready libraries for that purpose, unlike Ada/SPARK. Hopefully, it will be there, just not yet. It still requires tremendous multi-year effort to finish that.
- galangalalgol 5y agoIn addition to lacking formal verification tools, I'm worried about compiler certification with a language that changes as fast as rust, and c++, and even c now do. Yes you cannstick to a version, but the world and bug fixes, and libraries will pass you by. Which brings up another problem with rust for safety critical. The stdlib is so very thin, that doing almost anything requies a dependency tree of a dozen or more crates by different authors. You need to certify all those as well. Its a nightmare of an ecosystem from the safety cert perspective.
- steveklabnik 5y agoBe that as it may, it hasn't stopped certification from being pursued.
- galangalalgol 5y agoMany cases when you want cert will probably be nostd anyway so it is definitely worth pursuing given all the other advantages the language has. I'm just being grumpy because I love the language but I am a fan of batteries included languages. Or at least a thick stdlib and a boost-like thing. That is partly influenced by my primary dev environment being airgapped, and my secondary one being behind nexus/solarcube.