そこでSPARKですよ
SPARKは整数オーバーフローや配列の範囲外アクセスが絶対に起きないことを保証します
Rustにはそれができません、Rustはミッションクリティカルなシステムでは使い物になりません