5 ms·

NASA Ogma: generate hard-realtime C runtime monitoring applications

116 points by runeks 5y ago

rad_gruchalski 5y ago
I'm looking at the list of NASA repos and thinking to myself: why am I still not able to follow an organization on github? It's almost 2022 and it's still not possible.
b20000 5y ago
rust enthousiasts arriving in 3…2…1…
WJW 5y ago
For those without a NASA-level drone at home that still want to play around with generating hard-realtime C code, there is the excellent arduino-copilot package (https://hackage.haskell.org/package/arduino-copilot https://hackage.haskell.org/package/arduino-copilot) that does exactly what the name implies. I wrote a blog post about it at https://wjwh.eu/posts/2020-01-30-arduino-copilot.html https://wjwh.eu/posts/2020-01-30-arduino-copilot.html.
- ivanperez-keera 5y ago
  +1. For those wondering what the connection is: Ogma generates Copilot code, which you can compile to Arduino. But you can also of course write Copilot code directly.
  - sitkack 5y ago
    Thank you for such a wonderful readme!
    - ivanperez-keera 5y ago
      That's very kind of you! I do try to make my READMEs very clear, so I'm glad someone noticed! :)
  - i_don_t_know 5y ago
    I find this space fascinating. Can you recommend books or other resources to learn more about hard real-time systems, modeling and model-checking, and hardware-in-the-loop testing?
    - ivanperez-keera 5y ago
      That's an excellent question. The truth is that I do not know. What I didn't pick up during my uni studies, I did just through work. I'd love to hear other suggestions that people have. Specifically for the topic of this repo, we have a bunch of papers on Copilot, and related topics (FRP). I generally try to make the papers very accessible. I don't want to spam, but I can add the links if you think that may be interesting.
      - i_don_t_know 5y ago
        I looked around on the Copilot page and found a link to the papers: https://github.com/Copilot-Language/copilot-discussion https://github.com/Copilot-Language/copilot-discussion You might consider adding a Publications or Papers section to the documentation page that links directly to the PDFs. (But the link to the repo is fine too!) Very nice project!
- pizza 5y ago
  If I recall correctly, Galois also got involved in a DARPA initiative a few years back (HACMS [0]) to create un-hackable UAVs (drones) - use the Haskell type system to produce non-vulnerable C code [0] https://galois.com/project/hacms-high-assurance-cyber-military-systems/ https://galois.com/project/hacms-high-assurance-cyber-milita...
deleted 5y ago
[deleted]
martini333 5y ago
I hate Material Design with a passion. It's so off putting and ugly.
- black_13 5y ago
  What is „Material Design“?
deleted 5y ago
[deleted]
hydroxideOH- 5y ago
Pretty cool. I didn't know there were groups using Haskell at NASA.
- ivanperez-keera 5y ago
  AFAIK, there is only ours.
  - ivanperez-keera 5y ago
    I hope now that the world is coming back from the pandemic, we get to do conferences again. I've been missing giving talks. I'd love to present Ogma, and also explain what the challenges of using Haskell at NASA have been.
    - makira 5y ago
      What's the status of Rust usage inside NASA? I am currently writing software that, hopefully, will be sent to the Moon one day, and I am considering options as to software technologies.
      - ivanperez-keera 5y ago
        I do not really know. I heard that it's generally perceived as a good option, but I don't know if any teams are actively using it for any missions. My suspicion is that once it's generally accepted as part of the kernel, things may change. If the rust community wants rust to be used in safety-critical, my personal view is that they need to prioritize robustness and stability of the rust ecosystem as a whole over frequent changes to the language or libraries to save 1-2 lines of code. Breaking changes to APIs and tool changes are a big issue in general, so they are best avoided (almost every time some introduces a breaking change that we are forced to adopt, we have to spend thousands of dollars (in time) to adapt). It's best to take longer to release a tool, but when you do it, make sure it'll work for a long time. We recently had this case with a tool and our project was delayed by several weeks because someone replaced a version of a tool in homebrew that introduced a breaking change. We hit multiple bugs during the upgrade. A mission that flies won't depend on homebrew, but it would be very plausible for a bug to be fixed in a version that pulls a dependency with a higher version number, and for it to be impossible or impractical to upgrade only one or two packages. In particular (and I don't "speak" rust), if your compiler comes with core libraries that necessarily need a version of the compiler to work, you want those to be de-coupled and the core API not to change. Please be aware that this is just my personal opinion. I don't speak on behalf of any agencies.

116 points by runeks 5y ago

I'm looking at the list of NASA repos and thinking to myself: why am I still not able to follow an organization on github? It's almost 2022 and it's still not possible.

b20000 5y ago

rust enthousiasts arriving in 3…2…1…

WJW 5y ago

For those without a NASA-level drone at home that still want to play around with generating hard-realtime C code, there is the excellent arduino-copilot package (https://hackage.haskell.org/package/arduino-copilot https://hackage.haskell.org/package/arduino-copilot) that does exactly what the name implies. I wrote a blog post about it at https://wjwh.eu/posts/2020-01-30-arduino-copilot.html https://wjwh.eu/posts/2020-01-30-arduino-copilot.html.

ivanperez-keera 5y ago
+1. For those wondering what the connection is: Ogma generates Copilot code, which you can compile to Arduino. But you can also of course write Copilot code directly.
- sitkack 5y ago
  Thank you for such a wonderful readme!
  - ivanperez-keera 5y ago
    That's very kind of you! I do try to make my READMEs very clear, so I'm glad someone noticed! :)
- i_don_t_know 5y ago
  I find this space fascinating. Can you recommend books or other resources to learn more about hard real-time systems, modeling and model-checking, and hardware-in-the-loop testing?
  - ivanperez-keera 5y ago
    That's an excellent question. The truth is that I do not know. What I didn't pick up during my uni studies, I did just through work. I'd love to hear other suggestions that people have. Specifically for the topic of this repo, we have a bunch of papers on Copilot, and related topics (FRP). I generally try to make the papers very accessible. I don't want to spam, but I can add the links if you think that may be interesting.
    - i_don_t_know 5y ago
      I looked around on the Copilot page and found a link to the papers: https://github.com/Copilot-Language/copilot-discussion https://github.com/Copilot-Language/copilot-discussion You might consider adding a Publications or Papers section to the documentation page that links directly to the PDFs. (But the link to the repo is fine too!) Very nice project!
pizza 5y ago
If I recall correctly, Galois also got involved in a DARPA initiative a few years back (HACMS [0]) to create un-hackable UAVs (drones) - use the Haskell type system to produce non-vulnerable C code [0] https://galois.com/project/hacms-high-assurance-cyber-military-systems/ https://galois.com/project/hacms-high-assurance-cyber-milita...

deleted 5y ago

[deleted]

martini333 5y ago

I hate Material Design with a passion. It's so off putting and ugly.

black_13 5y ago
What is „Material Design“?

deleted 5y ago

[deleted]

hydroxideOH- 5y ago

Pretty cool. I didn't know there were groups using Haskell at NASA.

ivanperez-keera 5y ago
AFAIK, there is only ours.
- ivanperez-keera 5y ago
  I hope now that the world is coming back from the pandemic, we get to do conferences again. I've been missing giving talks. I'd love to present Ogma, and also explain what the challenges of using Haskell at NASA have been.
  - makira 5y ago
    What's the status of Rust usage inside NASA? I am currently writing software that, hopefully, will be sent to the Moon one day, and I am considering options as to software technologies.
    - ivanperez-keera 5y ago
      I do not really know. I heard that it's generally perceived as a good option, but I don't know if any teams are actively using it for any missions. My suspicion is that once it's generally accepted as part of the kernel, things may change. If the rust community wants rust to be used in safety-critical, my personal view is that they need to prioritize robustness and stability of the rust ecosystem as a whole over frequent changes to the language or libraries to save 1-2 lines of code. Breaking changes to APIs and tool changes are a big issue in general, so they are best avoided (almost every time some introduces a breaking change that we are forced to adopt, we have to spend thousands of dollars (in time) to adapt). It's best to take longer to release a tool, but when you do it, make sure it'll work for a long time. We recently had this case with a tool and our project was delayed by several weeks because someone replaced a version of a tool in homebrew that introduced a breaking change. We hit multiple bugs during the upgrade. A mission that flies won't depend on homebrew, but it would be very plausible for a bug to be fixed in a version that pulls a dependency with a higher version number, and for it to be impossible or impractical to upgrade only one or two packages. In particular (and I don't "speak" rust), if your compiler comes with core libraries that necessarily need a version of the compiler to work, you want those to be de-coupled and the core API not to change. Please be aware that this is just my personal opinion. I don't speak on behalf of any agencies.