That’s a Cheetah wearing an M1 helmet. Yeah, SPARK/Ada is that goofy. Pascal was considered unsafe for military projects, so they made Ada. Then Ada was considered unsafe for military projects, so they made SPARK, lulz.
Modern languages with type safety include Haskell, OCaml, and Coq. Because our critical systems are too precious for antiquated technology.
