Ada/SPARK is laughing at your 'safe programming language'.
Show me an OS written in Ada/SPARK and I'll take it seriously. Not this warmed-over, basically-modern-C++-language with worse syntax and a much weaker type system courtesy of inferred typing instead of strong typing.
I guess they expect that this will replace Linux any day now, right? I guess Linus et al better start rethinking their disdain of non-C languages lest they get left behind in the Rust-revolution.