It would be. Especially with mature tooling available from AdaCore. Seem my reply to vertex-four for links containing proof. Here's some examples in industry &

It would be. Especially with mature tooling available from AdaCore. Seem my reply to vertex-four for links containing proof. Here's some examples in industry & CompSci just for kicks: http://www.adacore.com/customers http://www.adacore.com/customers Note that the authors are just doing research on seeing how well Rust handles the problem domain. There's nothing wrong with them avoiding Ada to explore another tool or problem area. They should consider each carefully if they were trying to pick best tool for real work.