Потому, что для менее удобен, и есть много готовых решений на аде. Ну и надежность в долгосрочной перспективе, её он гарантировать не может.
И то, что в расте допустимо, тот же unsafe, в Аде - нет. Будет ругаться компилятор. Он очень много ругается.
Так же есть формальная верификация из коробки. Одна из самых удобных на текущий день.
Frama-C сосет у SPARK, заглатывая.
P.S. имела место быть опечаточка, перепутал мисру и frama-c. Сорян, до сих пор не оклемался после амнезии.