Bringing Rust to Safety-Critical Systems in Space
arxiv.org
arxiv.org
Why wouldn't they use Ada/SPARK2014? They have a published language standard, verification tools, and 25 years of applied use for mission-critical, high-integrity software.
The current state of Rust is a moving target for such tools and design methods. Publish a formal language standard first.
There's also HighTec's compiler that is also ISO 26262 qualified, targeting Infineo's Aurix TriCore:
https://www.infineon.com/cms/en/about-infineon/press/market-...
Not sure tho' what kind of qualification you have to look at in order to fly into space (DO... something?), this is targeting automotive ( and so is Ferrocene's). But a lot of the integrity mechanisms these MCU's have are surely similar between applications.
And... I'll be honest. I really am not convinced by the qualification itself that the quality is necessarily better. It's just that you need it for certain applications.
You don't need a formal language standard to make Rust usable for safety-critical areas. You do need a formally specified language for the certification, but it doesn't have to be official because heck, you need much more than a mere formally specified language anyway as you've just said. An expanded version of Ferrocene would just fit the bill for example.
I think some people are obsessed about the "formal" specification or the language "standard" because they are misunderstanding their effects. They are absolutely nothing without additional supports. A "formal" specification in this context is not really mathematically formal (like, say, WebAssembly [1]); it merely means that a specification is written in clearly defined terms and logically decomposable statements. A language "standard" is useless if it isn't or can't be enforced, and it doesn't even require the (non-mathematical) formality (though most standard organizations would demand that). As for now, the Rust language specification is "formal" and "standard" enough to be useful for language users, while it remains useful for third-party implementors but they can still find some gaps here and there.
Did anyone specify wasm using something like Coq, Lean or Isabelle/HOL?
But on this specific question, https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verif... is the work I am aware of.
[1] https://webassembly.github.io/spec/core/valid/instructions.h...
Would it be just easier to use something like OCaml? where it offers the memory safety and a mature language.
They tried but they were on the "nightly" branch of the standard and the compiler was on the "release" branch and then the compiler refused to compile the "nightly" standard because "nightly". /s
I worked for a space-related defense contractor. They are using MISRA C, and everything is very thoroughly designed, documented, and tested. I haven’t seen any research into bugs in safety critical systems caused by memory safety issues, but I think that in practice it is very possible to write memory safe C code if you follow industry standards.
There is a growing number of people and organizations that do see Rust as bringing advantages in this area.
That said, your parent isn’t wrong that the safety critical space has developed numerous ways of mitigating the risk of writing software, no matter what language it’s written in. But that doesn’t mean that language is irrelevant.
> Dir 4.12 Dynamic memory allocation shall not be used
> Rule 2.2 There shall be no dead code
https://github.com/sakura1083841400/MISRA-C/blob/main/MISRA%...
This provides nothing approaching the guarantees of safe Rust, as far as I can tell.