3 ms·
Before reading the report, I never thought about languages needing to be proven for space. I thought this was only a thing for hardware components.
by ahmedfromtunis 3y ago
Before reading the report, I never thought about languages needing to be proven for space. I thought this was only a thing for hardware components.
- steveklabnik 3y agoIn the sense they're talking about, they don't mean "formal proof," they mean "existence proof." It's not like it's a mature choice in the space, is what they mean.
- AceJohnny2 3y agoYeah, MISRA C [1] is a set of rules for writing C for safety-critical environments, originally targeting the automotive environment. If you're used to vanilla C, it can feel very constraining! In the Rust world, there's the Ferrocene project [2], which aims to provide a similar kind of safety-critical level of functionality. [1] https://en.wikipedia.org/wiki/MISRA_C https://en.wikipedia.org/wiki/MISRA_C [2] https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/ferrocene/
- steveklabnik 3y agoMISRA and Ferrocene are not really related other than both being vaguely in the safety space. MISRA is, as you say, a set of rules for writing C code, that restrict what you can do. Ferrocene is a qualified compiler. You write any normal Rust code you want: it's still the upstream Rust compiler. There are no restrictions. Incidentally, someone has compared what MISRA does to what Rust does: https://github.com/PolySync/misra-rust/blob/master/MISRA-Rules.md https://github.com/PolySync/misra-rust/blob/master/MISRA-Rul... Given that they can't repeat the MISRA stuff there, it's a bit disjoined, but it sure is interesting!
- AceJohnny2 3y agoThanks for the clarification Steve!