4 ms·

>>>However, due to its relatively short lifespan, industry adaption in safety-critical environments is still lacking. This work provides a set of recommendation

by eggy 2y ago

>>>However, due to its relatively short lifespan, industry adaption in safety-critical environments is still lacking. This work provides a set of recommendations for the development of safety-critical space systems in Rust. 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. https://www.adacore.com/about-spark https://www.adacore.com/about-spark

selfmodruntime 2y ago
There is a qualified and formally verified compiler called ferrocene [1]. [1]: https://ferrocene.dev/en/ https://ferrocene.dev/en/
- AlotOfReading 2y ago
  Ferrocene notably doesn't support any safety critical CPUs in its current qualification, and those that are experimental only support bare metal. It's exciting, but not at quite the same level of maturity yet.
  - RealityVoid 2y ago
    I'm pretty sure that there are safety critical ARM CPU's and Ferrocene does support ARM.
    - AlotOfReading 2y ago
      The R cores are not on the supported target list, they're on the experimental target list. See for yourself: https://public-docs.ferrocene.dev/main/user-manual/targets/index.html https://public-docs.ferrocene.dev/main/user-manual/targets/i...
      - RealityVoid 2y ago
        I stand corrected. I spoke before I checked my info. 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-news/2024/INFATV202404-089.html 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.
- lifthrasiir 2y ago
  Nit: it's formally specified, not formally verified (which is a really rare and difficult feat in comparison).
lifthrasiir 2y ago
> Publish a formal language standard first. 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. [1] https://webassembly.github.io/spec/core/ https://webassembly.github.io/spec/core/
- nextaccountic 2y ago
  The linked spec of wasm is written in English. Can we even say it's "formal"? Did anyone specify wasm using something like Coq, Lean or Isabelle/HOL?
  - steveklabnik 2y ago
    I agree that people mis-use the “formal” word when it comes to specifications. But on this specific question, https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verifying-the-webassembly-specification.pdf https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verif... is the work I am aware of.
  - lifthrasiir 2y ago
    WebAssembly is specified in an English prose and a formal notation, as you can see from, for example, [1]. It is still true that a (mathematically) formal specification can suffer from bugs due to the lack of verification, but it is much easier to verify an already formal specification than a prose specification. It is also possible to turn a prose into a formal specification if the prose in question is already close enough to the formal notation, like ESMeta [2]. [1] https://webassembly.github.io/spec/core/valid/instructions.html https://webassembly.github.io/spec/core/valid/instructions.h... [2] https://github.com/es-meta/esmeta https://github.com/es-meta/esmeta
vmfunction 2y ago
>The current state of Rust is a moving target for such tools and design methods. Publish a formal language standard first. Would it be just easier to use something like OCaml? where it offers the memory safety and a mature language.
- dequan 2y ago
  Garbage collection seems like a significant no-go for many safety critical systems. Other oddities like 31 and 63 bit numbers probably aren't a big deal but are still weird. "Mature" seems like a stretch when OCaml only got proper multi threading 1.5 years ago.
hulitu 2y ago
>Publish a formal language standard first. 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

by eggy 2y ago

selfmodruntime 2y ago

There is a qualified and formally verified compiler called ferrocene [1]. [1]: https://ferrocene.dev/en/ https://ferrocene.dev/en/

AlotOfReading 2y ago
Ferrocene notably doesn't support any safety critical CPUs in its current qualification, and those that are experimental only support bare metal. It's exciting, but not at quite the same level of maturity yet.
- RealityVoid 2y ago
  I'm pretty sure that there are safety critical ARM CPU's and Ferrocene does support ARM.
  - AlotOfReading 2y ago
    The R cores are not on the supported target list, they're on the experimental target list. See for yourself: https://public-docs.ferrocene.dev/main/user-manual/targets/index.html https://public-docs.ferrocene.dev/main/user-manual/targets/i...
    - RealityVoid 2y ago
      I stand corrected. I spoke before I checked my info. 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-news/2024/INFATV202404-089.html 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.
lifthrasiir 2y ago
Nit: it's formally specified, not formally verified (which is a really rare and difficult feat in comparison).

lifthrasiir 2y ago

> Publish a formal language standard first. 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. [1] https://webassembly.github.io/spec/core/ https://webassembly.github.io/spec/core/

nextaccountic 2y ago
The linked spec of wasm is written in English. Can we even say it's "formal"? Did anyone specify wasm using something like Coq, Lean or Isabelle/HOL?
- steveklabnik 2y ago
  I agree that people mis-use the “formal” word when it comes to specifications. But on this specific question, https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verifying-the-webassembly-specification.pdf https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verif... is the work I am aware of.
- lifthrasiir 2y ago
  WebAssembly is specified in an English prose and a formal notation, as you can see from, for example, [1]. It is still true that a (mathematically) formal specification can suffer from bugs due to the lack of verification, but it is much easier to verify an already formal specification than a prose specification. It is also possible to turn a prose into a formal specification if the prose in question is already close enough to the formal notation, like ESMeta [2]. [1] https://webassembly.github.io/spec/core/valid/instructions.html https://webassembly.github.io/spec/core/valid/instructions.h... [2] https://github.com/es-meta/esmeta https://github.com/es-meta/esmeta

vmfunction 2y ago

>The current state of Rust is a moving target for such tools and design methods. Publish a formal language standard first. Would it be just easier to use something like OCaml? where it offers the memory safety and a mature language.

dequan 2y ago
Garbage collection seems like a significant no-go for many safety critical systems. Other oddities like 31 and 63 bit numbers probably aren't a big deal but are still weird. "Mature" seems like a stretch when OCaml only got proper multi threading 1.5 years ago.

hulitu 2y ago

>Publish a formal language standard first. 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