4 ms·

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 ar

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.

bri3d 6y ago
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.
cat199 6y ago
> 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
- carlmr 6y ago
  I think this is spot on. The tooling is there for C++, but human mistakes are much more prevalent, and the discipline to apply the tooling is not a given. There should be an industry push for certified Rust tooling, it would save the aerospace and auto industry billions. Or you could use the unsexy but also very good ADA 2012, which is already certified.
  - pjmlp 6y ago
    This is one of the reasons why NVidia went with Ada/SPARK for their security critical firmware project.
    - sterlind 6y ago
      iirc, SPARK has proof capabilities that outstrip the memory-safety guarantees of Rust. basically design by contract, where you can check loop invariants and statically verify complex preconditions and postconditions. I suppose the workflow would be to flesh out and check the abstract design in something like Coq or (maybe) TLAPS, generate a refinement into the SPARK code contracts, then implement the functions. Since the toolchains are verified there shouldn't be much surface area for bugs left.
      - pjmlp 6y ago
        Yep, here some very good books about it, specially relevant given the main subject. "Building High Integrity Applications with SPARK" https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107656842 https://www.amazon.com/Building-High-Integrity-Applications-... "Building Parallel, Embedded, and Real-Time Applications with Ada" https://www.amazon.com/Building-Parallel-Embedded-Real-Time-Applications/dp/0521197163 https://www.amazon.com/Building-Parallel-Embedded-Real-Time-... "Embedded Software Development for Safety-Critical Systems" https://www.amazon.com/Embedded-Software-Development-Safety-Critical-Systems/dp/0367338858 https://www.amazon.com/Embedded-Software-Development-Safety-...
gregors 6y ago
Here's a pretty interesting read regarding Lisp at JPL. http://www.flownet.com/gat/jpl-lisp.html 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_incident https://en.wikipedia.org/wiki/Iran%E2%80%93U.S._RQ-170_incid...

bri3d 6y ago

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.

cat199 6y ago

> 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

carlmr 6y ago
I think this is spot on. The tooling is there for C++, but human mistakes are much more prevalent, and the discipline to apply the tooling is not a given. There should be an industry push for certified Rust tooling, it would save the aerospace and auto industry billions. Or you could use the unsexy but also very good ADA 2012, which is already certified.
- pjmlp 6y ago
  This is one of the reasons why NVidia went with Ada/SPARK for their security critical firmware project.
  - sterlind 6y ago
    iirc, SPARK has proof capabilities that outstrip the memory-safety guarantees of Rust. basically design by contract, where you can check loop invariants and statically verify complex preconditions and postconditions. I suppose the workflow would be to flesh out and check the abstract design in something like Coq or (maybe) TLAPS, generate a refinement into the SPARK code contracts, then implement the functions. Since the toolchains are verified there shouldn't be much surface area for bugs left.
    - pjmlp 6y ago
      Yep, here some very good books about it, specially relevant given the main subject. "Building High Integrity Applications with SPARK" https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107656842 https://www.amazon.com/Building-High-Integrity-Applications-... "Building Parallel, Embedded, and Real-Time Applications with Ada" https://www.amazon.com/Building-Parallel-Embedded-Real-Time-Applications/dp/0521197163 https://www.amazon.com/Building-Parallel-Embedded-Real-Time-... "Embedded Software Development for Safety-Critical Systems" https://www.amazon.com/Embedded-Software-Development-Safety-Critical-Systems/dp/0367338858 https://www.amazon.com/Embedded-Software-Development-Safety-...

gregors 6y ago

Here's a pretty interesting read regarding Lisp at JPL. http://www.flownet.com/gat/jpl-lisp.html 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_incident https://en.wikipedia.org/wiki/Iran%E2%80%93U.S._RQ-170_incid...