It wasn't a mistake for Rust not to emphasise formal verification. Going that route would have been very restrictive. Rust is aiming to offer a safer alternativ

It wasn't a mistake for Rust not to emphasise formal verification. Going that route would have been very restrictive. Rust is aiming to offer a safer alternative to C, not a more approachable formally verifiable language. That said, it looks like the good ideas from Rust may find their way into SPARK, a highly restrictive programming language for critical systems development with formal verification. [0][1] [0] https://www.adacore.com/papers/safe-dynamic-memory-management-in-ada-and-spark https://www.adacore.com/papers/safe-dynamic-memory-managemen... [1] https://arxiv.org/abs/1805.05576 https://arxiv.org/abs/1805.05576