5 ms·

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).