It's cool that this framework is getting some attention. In our college senior design project, we built a small prototype using this framework during a trade study. We got a few small UI fixes pushed upstream to the main repo. Our team even got to meet up with the maintainers for a few days as they were showing off the framework. It was one of the most interesting and unique software projects I've worked on.
The framework itself is portable allowing for code sharing across multiple missions and hardware setups. According to the devs, in the space industry, software is so mission specific and intertwined that it's rarely reused. FPrime's "modules" create hard barriers between sections of the program, something I have mixed feelings about. Finally the "module" system allows for a very easy to use concurrency model, which I think is one of the strengths of the framework. (Though, take these words with a grain of salt as I was and still am wildly underqualified in the domain of embedded systems)
If they were planning to open-source this all along, I'm curious if Ardupilot  would have worked for this. The Ardupilot flight stack is quite mature for Earth-based aircraft, I suppose they could make it work for Mars with a few modifications.
So it’s ROS replacement that doesn’t suck?
Can you elaborate more on this?
How long before Rust will be mature enough for the task?
Keep in mind that for this kind of project you want static analysis and formal verification (model checking for example) rather than just day-to-day safety features.
I.e. the Rust this, Rust that spam is a little naive to the task at hand, even though it would be a step up from C
NASA even has their own sound static analyzer for memory safety. If you use something like that, and depending on the context, there isn't even necessarily a memory safety advantage to using Rust over C or C++.
It was my understanding that when formal methods were used, they were used on very small subsets of code and not used in general. I do wonder about TLA+ and would love to hear more about how they use such tools.
I know I've seen an older document that specifically prohibited use of malloc that the risk was too great. Is that still the case?
Formal methods are indeed hard. They generally thrive on hardware, software is a wholly different kettle of fish in terms of the size of the problem (the actual methods are often similar, but hardware design generally encourages certain patterns that are easier to analyse)
I'm not related to this project or aerospace, so I can't divine more knowledge than anyone else, although I have seen many coding standards that forbid malloc after some critical time (e.g. no dynamic memory allocation after the plane is off the ground)
Is C++ complex enough that it is difficult to model, and therefore hard to apply in formal methods?
The problem is not the language, the problem are unbounded loops. Like linked lists vs vectors. Termination is theoretically impossible to prove, but practically you can handle it.
Parts of the STL were formally verified. cprover (with satabs and cbmc) can handle C, C++ or Java. F' uses autogenerated classes, which helps a lot avoiding mistakes.
a) probably the least important class of bugs for this sort of thing
b) adequately solved with the existing C++ language features anyways.
So what would be the point of rewriting in Rust?
(Assume the people writing it aready have the C++ knowledge and tooling ready.)
What about iterator invalidation or multiple mutable aliasing in concurrent code
Probably once people have decades of experience with it and know every single trap or quirk perfectly.
Rust almost certainly could do the job now but stakes are so high no one would take that risk when its proven that C can do it and with enough auditing and conservatism, it can be done pretty safely.
Here's a pretty interesting read regarding Lisp at JPL. http://www.flownet.com/gat/jpl-lisp.html
I think the "safety" of "familiarity" vs pushing the envelope of what we can do technically are different things. We used to build brand new computers and operating systems from scratch specifically for these types of things.
The risks are indeed high for managerial staff. I worked at a large quasi-government place. "you won't ever get fired for using Microsoft, Oracle, etc" was a tagline we heard often in non-critical systems, so I imagine there would need to be some major technical reason to switch.
Now drones on the other hand... https://en.wikipedia.org/wiki/Iran%E2%80%93U.S._RQ-170_incid...
I don't think the barrier is _people_ knowing the traps, as people are always fallible and any system relying on them knowing the "traps and quirks" is fundamentally pointless. I do think the barrier is, rather, _tools_ knowing the traps. Most systems in this class, FPrime included, rely extensively on code generation and model-to-code auditing, which, while usually not formally proven (unfortunately), is battle-tested.
Now, these sorts of systems should actually be _easier_, in the long-term, to build in Rust, since the type system can enable a class of proof which simply was not historically possible, but for the time being, the tooling doesn't exist yet.
> Probably once people have decades of experience with it and know every single trap or quirk perfectly.
people were writing mission-critical C++ when C++ was new / only a few years old; with this in mind, rust is probably good to go with sufficient application/system testing
that said, since C++ & associated tooling exists, there is more of an opportunity cost since, in the context of today, there are more alternatives that could be considered
Never. Rust will never be good enough to replace C.
this is c++
Get a daily email with the the top stories from Hacker News. No spam, unsubscribe at any time.