[Raphael_Amiard]

SPARK allows you to formally prove that your code is correct according to a given specification. It can thus provides much stronger guarantees than what Rust would be able to provide.

Similar technology exists for Rust, but it is much less advanced than SPARK is (https://github.com/xldenis/creusot)