6 ms·

Re-written: I'm surprised Bash shell passed muster for mission critical NASA applications given it isn't based on a formally verifiable language that they tend

Re-written: I'm surprised Bash shell passed muster for mission critical NASA applications given it isn't based on a formally verifiable language that they tend to use (e.g. Ada).

saurik 5y ago
https://www.pcmag.com/news/linux-is-now-on-mars-thanks-to-nasas-perseverance-rover https://www.pcmag.com/news/linux-is-now-on-mars-thanks-to-na... > Linux Is Now on Mars, Thanks to NASA's Perseverance Rover > Previous NASA Mars rovers mostly used an operating system from Wind River Systems. But this time, the space agency chose Linux for Perseverance's Ingenuity helicopter drone. https://linuxunplugged.com/396 https://linuxunplugged.com/396 > [audio] Tim Canham, the Mars Helicopter Operations Lead, shares Linux’s origins at JPL and how it ended up running on multiple boxes on Mars.
- mst 5y ago
  I know one of the DoD sysadmins who was involved in making this happen, and have taken great joy in listening to her brag about it any time she likes. Never gets old for me :D
dooglius 5y ago
From what I've read, one of the things the helicopter project did was to see how well ignoring the usual heavy verification would go--it used consumer-grade off-the-shelf hardware as well, for instance.
- capableweb 5y ago
  > From what I've read Could you recall any sources to this? Just because they are using OTS hardware doesn't mean it doesn't go through verification and testing, it just means they are buying hardware instead of making it themselves.
  - deleted 5y ago
    [deleted]
  - _joel 5y ago
    They have 2 sets of RAM and a RAD hardened FPGA that checks for bitfips in the memory. It can restart one that quickly that it can do it mid-flight. It's amazing what possibilities this could open up as doing intensive image processing on RAD hardened is expensive, or not even possible as it lags behind the state of the art. edit: found the paper https://trs.jpl.nasa.gov/bitstream/handle/2014/46229/CL%2317-6243.pdf https://trs.jpl.nasa.gov/bitstream/handle/2014/46229/CL%2317...
  - samizdis 5y ago
    There's this recent-ish news article: How the First Helicopter on Mars Uses Off-the-Shelf Hardware and Linux https://thenewstack.io/how-the-first-helicopter-on-mars-uses-off-the-shelf-hardware-and-linux/ https://thenewstack.io/how-the-first-helicopter-on-mars-uses...
capableweb 5y ago
"I stopped at", saying software on a flying helicopter on Mars "isn't mission critical" and that bash would never pass any verification process at NASA does indeed sound like you're dissing bash here. If your intent was to leave some sort of feedback or opinion that can improve things and look less like a "diss", then you probably wanna give it another go.
- deleted 5y ago
  [deleted]
- SavantIdiot 5y ago
  Better?
nexuist 5y ago
Why would you be surprised? Out of nearly a decade of using Bash on Linux I don't think I have ever run into a bash bug or issue. There's been bugs with utilities like sudo of course, but those aren't Bash.
- chasil 5y ago
  From the anguish of those who try to implement the POSIX shell, I understand that edge cases are far from difficult to find. The Almquist shell (Debian Dash) is cited for not using lex/yacc to implement the parser, and described as untrustworthy. https://archive.fosdem.org/2018/schedule/event/code_parsing_posix_s_hell/ https://archive.fosdem.org/2018/schedule/event/code_parsing_... A major goal of this later ADA implementation is readability, in addition to (Windows) performance and ADA's safety. https://archive.fosdem.org/2019/schedule/event/ada_shell/ https://archive.fosdem.org/2019/schedule/event/ada_shell/
- SavantIdiot 5y ago
  "I don't think I have ever run into a bash bug or issue." That is not a statement about a formally verifiable program that I would base a billion-dollar program on.
  - varjag 5y ago
    Ariane 5 bug was formally verified.
    - sigzero 5y ago
      No it really wasn't.
  - count 5y ago
    Formally verified programs often still have bugs. AWS S2N, for example, currently has hundreds of open issues and identified bugs, despite being the subject of a continuous formal verification program. Bash powers probably hundreds of billions of dollars worth of critical infrastructure...
  - 5y ago
tyingq 5y ago
Assuming a posix-ish shell were a requirement for some NASA mission, what shell do you think might pass their verification process?
- bitbang 5y ago
  /bin/true
fidesomnes 5y ago
surely this is what a CS degree perspective gives you.

Re-written: I'm surprised Bash shell passed muster for mission critical NASA applications given it isn't based on a formally verifiable language that they tend to use (e.g. Ada).

saurik 5y ago

https://www.pcmag.com/news/linux-is-now-on-mars-thanks-to-nasas-perseverance-rover https://www.pcmag.com/news/linux-is-now-on-mars-thanks-to-na... > Linux Is Now on Mars, Thanks to NASA's Perseverance Rover > Previous NASA Mars rovers mostly used an operating system from Wind River Systems. But this time, the space agency chose Linux for Perseverance's Ingenuity helicopter drone. https://linuxunplugged.com/396 https://linuxunplugged.com/396 > [audio] Tim Canham, the Mars Helicopter Operations Lead, shares Linux’s origins at JPL and how it ended up running on multiple boxes on Mars.

mst 5y ago
I know one of the DoD sysadmins who was involved in making this happen, and have taken great joy in listening to her brag about it any time she likes. Never gets old for me :D

dooglius 5y ago

From what I've read, one of the things the helicopter project did was to see how well ignoring the usual heavy verification would go--it used consumer-grade off-the-shelf hardware as well, for instance.

capableweb 5y ago
> From what I've read Could you recall any sources to this? Just because they are using OTS hardware doesn't mean it doesn't go through verification and testing, it just means they are buying hardware instead of making it themselves.
- deleted 5y ago
  [deleted]
- _joel 5y ago
  They have 2 sets of RAM and a RAD hardened FPGA that checks for bitfips in the memory. It can restart one that quickly that it can do it mid-flight. It's amazing what possibilities this could open up as doing intensive image processing on RAD hardened is expensive, or not even possible as it lags behind the state of the art. edit: found the paper https://trs.jpl.nasa.gov/bitstream/handle/2014/46229/CL%2317-6243.pdf https://trs.jpl.nasa.gov/bitstream/handle/2014/46229/CL%2317...
- samizdis 5y ago
  There's this recent-ish news article: How the First Helicopter on Mars Uses Off-the-Shelf Hardware and Linux https://thenewstack.io/how-the-first-helicopter-on-mars-uses-off-the-shelf-hardware-and-linux/ https://thenewstack.io/how-the-first-helicopter-on-mars-uses...

capableweb 5y ago

"I stopped at", saying software on a flying helicopter on Mars "isn't mission critical" and that bash would never pass any verification process at NASA does indeed sound like you're dissing bash here. If your intent was to leave some sort of feedback or opinion that can improve things and look less like a "diss", then you probably wanna give it another go.

deleted 5y ago
[deleted]
SavantIdiot 5y ago
Better?

nexuist 5y ago

Why would you be surprised? Out of nearly a decade of using Bash on Linux I don't think I have ever run into a bash bug or issue. There's been bugs with utilities like sudo of course, but those aren't Bash.

chasil 5y ago
From the anguish of those who try to implement the POSIX shell, I understand that edge cases are far from difficult to find. The Almquist shell (Debian Dash) is cited for not using lex/yacc to implement the parser, and described as untrustworthy. https://archive.fosdem.org/2018/schedule/event/code_parsing_posix_s_hell/ https://archive.fosdem.org/2018/schedule/event/code_parsing_... A major goal of this later ADA implementation is readability, in addition to (Windows) performance and ADA's safety. https://archive.fosdem.org/2019/schedule/event/ada_shell/ https://archive.fosdem.org/2019/schedule/event/ada_shell/
SavantIdiot 5y ago
"I don't think I have ever run into a bash bug or issue." That is not a statement about a formally verifiable program that I would base a billion-dollar program on.
- varjag 5y ago
  Ariane 5 bug was formally verified.
  - sigzero 5y ago
    No it really wasn't.
- count 5y ago
  Formally verified programs often still have bugs. AWS S2N, for example, currently has hundreds of open issues and identified bugs, despite being the subject of a continuous formal verification program. Bash powers probably hundreds of billions of dollars worth of critical infrastructure...
- 5y ago

tyingq 5y ago

Assuming a posix-ish shell were a requirement for some NASA mission, what shell do you think might pass their verification process?

bitbang 5y ago
/bin/true

fidesomnes 5y ago

surely this is what a CS degree perspective gives you.