I really wish there was more active development on SPARK.

It's largely untouched over the last 10-years.

https://github.com/AdaCore/spark2014

For those not aware, SPARK gives even more safeguards/guarantees than Rust (see below) ... and also does it at compile time (when not all of Rust safeguards are at compile time).

https://blog.adacore.com/should-i-choose-ada-spark-or-rust-o...