AdaCore and Ferrous Systems Joining Forces to Support Rust

This is exciting! I&#x27;ve met with people from AdaCore and Ferrous systems (individually) several times and they&#x27;re all serious, competent and motivated.<p>I&#x27;m curious what kinds of software they want to (eventually) verify, my PhD thesis is developing a verification tool for Rust (<a href="https:&#x2F;&#x2F;github.com&#x2F;xldenis&#x2F;creusot" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;xldenis&#x2F;creusot</a>) and I&#x27;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&#x27;s embedded Rust tooling is outstanding. Ie its [Knurling App template](<a href="https:&#x2F;&#x2F;github.com&#x2F;knurling-rs&#x2F;app-template" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;knurling-rs&#x2F;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&#x27;ve seen besides Arduino.

This is a very interesting move from AdaCore. I&#x27;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&#x27;s a language with a lot to offer.

This are big news, congratulations to everyone making this happen!<p>Looking forward to what it might bring into safer computing world.

I have no connections to AdaCore, but the products are absolutely great (especially GNAT community edition).

I hope someone also picks up the work started in <a href="https:&#x2F;&#x2F;project-oak.github.io&#x2F;rust-verification-tools&#x2F;" rel="nofollow">https:&#x2F;&#x2F;project-oak.github.io&#x2F;rust-verification-tools&#x2F;</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:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;AIM-120_AMRAAM" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;AIM-120_AMRAAM</a>

Can we get a Rust version of Spark now? I think that would be really cool!

Is Ferrocene going to be open source?

This is so wonderful that two companies so focused on reliability and safety are teaming up!<p>&gt; 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!

Soon a &quot;pragma Import (Rust, MyFunction);&quot; ? :)