Firstly, for any of the 4 projects that have been announced by Prossimo so far, a garbage collected language would be unsuitable as it would be rejected by almo

Firstly, for any of the 4 projects that have been announced by Prossimo so far, a garbage collected language would be unsuitable as it would be rejected by almost all current users of the respective projects. Given that, as you correctly point out there are still lots of options that could be used; for example, Ada/SPARK has been around and freely available via GNAT for a long time. For example, here is a DNS server implemented in Ada/SPARK: http://ironsides.martincarlisle.com/ http://ironsides.martincarlisle.com/ Latest download is 5 years old - can you find a single instance of IRONSIDES running in the wild? IMHO the main advantage that Rust has over other approaches that would technically work to create sufficiently secure software is that it has much lower barriers to entry and a much larger community - the hardest part of getting a technology adopted is marketing, and Rust is currently the only option that can compete with C/C++ here. There is already some promising work on formalizing the semantics of Rust, see for example https://plv.mpi-sws.org/rustbelt/popl18/ https://plv.mpi-sws.org/rustbelt/popl18/ and https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf