[Argorak]

I very much agree. Rust is often seen as C/C++-inspired, but I know a lot of the early team looked at Ada for inspiration. We have also seen in many evaluations of "new stacks" that we were invited in that Ada was evaluated along with Rust. The conclusion was often similar: both languages have matching ambitions, in different forms. Also, there's a ton of places where Ada is just "there" already, e.g. by having something like SPARK available and in production use for many years.

I expressed some of those thoughts in the corresponding post on the Ferrous Systems blog: https://ferrous-systems.com/blog/ferrous-systems-adacore-joi...

[zppln]

I'm curious as to what you see are the benefits of using Rust in high assurance applications, compared to the alternatives already available? In my experience (which doesn't include anything related to formal verification), when everything's said and done you're left with a fairly limited subset of your chosen language anyway.

[Argorak]

Rust makes quite a few things more rigorous (e.g. pairing allocations with deallocations and reference validity). It basically fulfills the job of a static analyzer baked into the language.

It's also a vastly more analyzable language (in that its syntax is reasonably unambiguous and there's no dynamic runtime in play) and it can be integrated well.

Toolchain quality (error reporting, built in testing, awareness of primitives like "libraries", etc.) is also a huge strong point.

We're reasonably confident that we can use safe Rust as is, with strong guidance on how to do unsafe Rust.

For a tangible investigation of that space, PolySync has a project that has a look at MISRA rules from a Rust perspective. https://github.com/PolySync/misra-rust/blob/master/MISRA-Rul...

Ada is a good example here: the language has not evolved something like MISRA-C (it has evolved SPARK for formal verification, but I see that differently).

[gmfawcett]

> Ada is a good example here: the language has not evolved something like MISRA-C (it has evolved SPARK for formal verification, but I see that differently).

This may interest you: "In this document, we show how SPARK can be used to achieve high code quality with guarantees that go beyond what would be feasible with MISRA C."

https://www.adacore.com/uploads/books/pdf/SPARK-Ada-for-MISR...

[zppln]

Interesting, thanks. The reason I ask is that in my experience you don't malloc mid-flight so to speak (for WCET/WCRU reasons, among others), so Rust's guarantees there are largely irrelevant. It's a pretty opaque area of the software industry though, so others may have come to other conclusions.

[steveklabnik]

I'm not working in safety critical systems, but our embedded OS doesn't do any dynamic memory allocation at all, and Rust still helps quite a bit even without that.

https://cliffle.com/blog/on-hubris-and-humility/

[Argorak]

DO-178C has writing and requirements around dynamic memory management. (DO-332 / ED-217, OO.D.1.6)

Rust also can also model other things through ownership, like passing a device handle safely between components, to avoid concurrent use.

[zppln]

Thanks, I wasn't aware of DO-332 actually. I'll have to see if it's available through work. It's always interesting to think about how things can be done differently and where the tradeoffs would be. :)

[Argorak]

Feel free to reach out, it's a topic of interest to us. A good place to discuss is for example the AeroRust Discord or just send me an email. https://github.com/AeroRust/Welcome

[mlindner]

Rust has the same advantages in malloc-free environments as well. Dangling pointers can still be a thing in non-malloc code.

[gameswithgo]

Compared to most other languages that focus on correctness, Rust performs better. If you don't need performance, probably one of the other alternatives is better. However Rust may be unique in preventing data races at compile time, which could be a huge boon in some applications.

I suppose languages like Haskell maybe accomplish that as well, since you never mutate state at all?

[mjw1007]

Is there going to be an announcement on the current status of Ferrocene soon? It's been almost a year since the last blog post.

In the meeting with the lang team last February, I think the consensus was that the next step would be to create a proposed charter for a project group. Did that happen?

[Argorak]

First question: yes. It was hard to talk about the current state of Ferrocene with all the things ongoing last year. Now that I have more bandwidth and we found a development beat, you can also expect more regular updates.

Second question: that was the discussion about higher assurances in the compiler in general. The group did not form, but that's on the project side, where I'm not part of anymore. We're very ready to participate there though.