This is exciting! I've met with people from AdaCore and Ferrous systems (individually) several times and they're all serious, competent and motivated.<p>I'm curious what kinds of software they want to (eventually) verify, my PhD thesis is developing a verification tool for Rust (<a href="https://github.com/xldenis/creusot" rel="nofollow">https://github.com/xldenis/creusot</a>) and I'm always on the look out for case studies to push me forward.<p>The road to formally verified Rust is still long but in my unbiased opinion looking quite bright, especially compared to other languages like C.
Ownership typing <i>really</i>, <i>really</i> simplifies verification.
Ferrous's embedded Rust tooling is outstanding. Ie its [Knurling App template](<a href="https://github.com/knurling-rs/app-template" rel="nofollow">https://github.com/knurling-rs/app-template</a>), and associated Probe-run, Deft, and flip-link.<p>These make flashing and debugging Rust embedded very easy - easier than any embedded toolchain I've seen besides Arduino.
This is a very interesting move from AdaCore. I've been a vocal advocate of Ada as a general purpose programming language for a little while. I hope that this helps expose the language to a wider audience, and gives the wider programming community cause to reappraise Ada from a modern perspective. It's a language with a lot to offer.
I hope someone also picks up the work started in <a href="https://project-oak.github.io/rust-verification-tools/" rel="nofollow">https://project-oak.github.io/rust-verification-tools/</a> - the idea of having a `cargo verify` tool that supports different backends is great for bridging the academic PoCs with something that an average programmer can integrate into the dev workflow.
Does this mean someone can program a AIM-120 AMRAAM missile in Rust instead of Ada?<p><a href="https://en.wikipedia.org/wiki/AIM-120_AMRAAM" rel="nofollow">https://en.wikipedia.org/wiki/AIM-120_AMRAAM</a>
This is so wonderful that two companies so focused on reliability and safety are teaming up!<p>> Ferrous Systems and AdaCore are announcing today that they’re joining forces to develop Ferrocene - a safety-qualified Rust toolchain, which is aimed at supporting the needs of various regulated markets, such as automotive, avionics, space, and railway.<p>Hoping for a long, fruitful relationship!<p>*edit, Yay!