10 ms·

Masten Space Systems is using Ada and Spark to land on the Moon's south pole [pdf]

StatsAreFun 5y ago
I wish I had more opportunity to use Ada. GNAT Studio can be buggy but the language itself and the safety it brings to software engineering is really nice to work with.
- mcculley 5y ago
  What language is GNAT Studio written in?
  - exdsq 5y ago
    Ada lol - think I see what you’re getting at there. GTK toolkit and python as an internal scripting language.
    - bigbizisverywyz 5y ago
      Kinda reminds me of the Rational suite of programs from early 2000's that did UML modelling and other aspects of software requirements & project management. They were some of the buggiest most crash-probe applications I've ever used, whilst the whole time their marketing trumpeted about how much better the quality of your software would be if you used them. Oh the irony!
okl 5y ago
> Ghosh says they’re trying to fully understand what they’re building before they start coding. This should be normal practice IMO.
- sjburt 5y ago
  I've seen this approach. The wrong thing still gets built, but at least you know why it was built that way.
  - mhh__ 5y ago
    "Thinking doesn't guarantee that we won't make mistakes. But not thinking guarantees that we will" - Leslie Lamport
    - butterisgood 5y ago
      Or, my favorite saying, "All these weeks of coding saved us literally hours of planning".
- ramesh31 5y ago
  >This should be normal practice IMO. Coding is the process of fully understanding what needs to be built. We've all seen architecture astronauts churn out reams of UML that still result in a broken system. Exploring the space via iterative MVP is far more productive.
  - deleted 5y ago
    [deleted]
  - jlg23 5y ago
    But when your deployment costs run into the 7 to 10 digit numbers, you might long for better peer review of your code. Formal proofs provide that.
    - zozbot234 5y ago
      The best application for formal proof is actually in lightweight sanity checks as opposed to "deep" review of your code. To put it very clearly, it should simply not be possible for a properly-engineered program to conflate feet w/ meters and crash a space probe as a direct result of that conflation. There's just no way that this is ever valid semantics.
      - p_l 5y ago
        interestingly, that's one of the areas where Ada shines, as you can define your own integer subtype that will help you preserve the semantics (and Ada has, iirc, no implicit casts, so it would require explicit cast to push feet into metres (and it might be made so that such cast would actually convert the values properly)
        okl 5y ago
        Ada subtypes are "compatible" in that you can implicitly convert them, you're referring to types.
    - actinium226 5y ago
olah_1 5y ago
I'm sure Ada makes a reliable program, but wouldn't it also be good to have an Erlang/Elixir style "self-healing" system with supervisors that can stop and restart each other?
- Jtsummers 5y ago
  That actually is done with a lot of these kinds of systems. In many of the ones I've worked on you have software or hardware "watchdog timers" that have to be reset, or a process will be terminated and restarted (how will vary a bit). Hardware watchdog timers usually trigger something like a reboot, causing the program to be reloaded and restarted. That's about the simplest you can make a supervisor, but you can have more complex ones monitoring the actual internals to respond should the state become corrupted in some fashion as well. https://en.wikipedia.org/wiki/Watchdog_timer https://en.wikipedia.org/wiki/Watchdog_timer
  - trothamel 5y ago
    The programs that ran on the Apollo Guidance Computer were written this way. If there was a sufficiently bad error, the AGC would restart execution. The programs took advantage of the memory in use at the time being non-volatile, and not reset to zero when the computer restarted, so the program could figure out what the CSM or LM was doing, and continue it. This actually happened on Apollo 11. The 1201 and 1202 program alarms were the computer overloading, and running out of space for more processes. When this happened, the computer would reset, and navigation would pick up again.
  - touisteur 5y ago
    To add to this, usually most of the systems in avionics or support systems on the ground are dual-hardware (when not more). There's lots of work done to ensure there's no single point of failure and hardware (and more and more, software) failures are handled safely. Regulators add every 5-10y some pressure on time-to-recovery and acceptable data of service loss (counted in milliseconds even on ground systems). Erlang didn't invent much there, and restarting/rebooting isn't always possible (try doing that in less than 10ms). Sometimes, the application itself needs to handle problems. This puts lots of 'classic IT' (interface bonding, fail overs, etc.) stuff to the bin very quick.
mLuby 5y ago
To be clear, they are not currently—nor have they ever—landed on the Moon. better: s/Is Using/Will Use/ best: s/Is Using/Intends to Use/
exdsq 5y ago
Anyone here using ADA? Seems really interesting
- rvnx 5y ago
  Airbus
- nextos 5y ago
  Altran / Praxis and AdaCore. Used in the software for e.g. French nuclear power plants and other safety-critical systems.
  - touisteur 5y ago
    Hi, do you have a source for the French nuclear plant use? Some kind of paper? Really interested in real-world applications of Spark and had never heard of such. To me the nuclear world was walled off with very specific tech, different than the stuff from rail or avionics.
    - nextos 5y ago
      I've worked on railway systems, but I didn't use Spark. I've seen many mentions to Spark being used in nuclear power software during conferences and presentations. But I'm afraid open materials might not be available... Here you can see some real uses of Spark listed: https://www.cse.chalmers.se/edu/year/2017/course/TDA294_Formal_Methods_for_Software_Development/Lectures/Files/aw_altran_spark_slides_sept_2017.pdf https://www.cse.chalmers.se/edu/year/2017/course/TDA294_Form...
      - touisteur 5y ago
        Thanks! I know of some rail projects in spark some colleagues worked on (and some internal company recruiting efforts) but I guess it's quite recent and maybe not yet deployed. I'll ask around about nuclear, thanks again!
- VygmraMGVl 5y ago
dandotway 5y ago
Ada's formal verification capabilities have fallen behind Frama-C for ANSI/ISO C. Frama-C allows formal verification of essentially arbitrary heap manipulation algorithms. You can implement linked lists and graphs in traditional C with Frama-C annotations in the comments, then prove your code never dereferences NULL, never has an integer overflow, etc. One single commercial Ada vendor offers Spark, a formally verifiable subset of Ada. Spark does not allow arbitrary dynamically allocated data structures like Frama-C does. https://frama-c.com/ https://frama-c.com/
- p_l 5y ago
  Seems that's no longer true, as current SPARK version permits pointers given they follow certain memory ownership policy.
  - dandotway 5y ago
    Yes, SPARK has a Rust-like borrow checker that doesn't allow implementing arbitrary pointer graphs. You have to use 'unsafe Rust' to implement linked list containers which, once implemented, other parts of the codebase can then consume in 'safe Rust'. Seems to be the same deal with SPARK ('safe Ada') vs vanilla Ada ('unsafe Ada').
    - p_l 5y ago
      Interestingly both Frama-C and SPARK use linked list as an example. But yes, not everything can be verified, though I'd rather bet on Ada than Rust in this area.
      - dandotway 5y ago
        The SPARK example I found uses singly-linked lists and says doubly-linked lists and graphs with cycles are not supported: https://blog.adacore.com/pointer-based-data-structures-in-spark https://blog.adacore.com/pointer-based-data-structures-in-sp... Yes, I could and should have been more explicit when I spoke of 'linked lists' without further qualification. While talking about these languages designed to eliminate all ambiguity I would do well to be unambiguous. :-)
smoyer 5y ago
Just a small gripe - this article shouldn't really be "How Masten Space ..." I think that story would be fascinating. This article is more of "Why" and "What" which is still worth reading.
bpodgursky 5y ago
Headline might want to indicate it's SPARK, not Spark (the Hadoop-ecosystem project). As someone with a lot of experience building systems in the big data space... I was very concerned for their lander.
deleted 5y ago
[deleted]

I wish I had more opportunity to use Ada. GNAT Studio can be buggy but the language itself and the safety it brings to software engineering is really nice to work with.

mcculley 5y ago
What language is GNAT Studio written in?
- exdsq 5y ago
  Ada lol - think I see what you’re getting at there. GTK toolkit and python as an internal scripting language.
  - bigbizisverywyz 5y ago
    Kinda reminds me of the Rational suite of programs from early 2000's that did UML modelling and other aspects of software requirements & project management. They were some of the buggiest most crash-probe applications I've ever used, whilst the whole time their marketing trumpeted about how much better the quality of your software would be if you used them. Oh the irony!

okl 5y ago

> Ghosh says they’re trying to fully understand what they’re building before they start coding. This should be normal practice IMO.

sjburt 5y ago
I've seen this approach. The wrong thing still gets built, but at least you know why it was built that way.
- mhh__ 5y ago
  "Thinking doesn't guarantee that we won't make mistakes. But not thinking guarantees that we will" - Leslie Lamport
  - butterisgood 5y ago
    Or, my favorite saying, "All these weeks of coding saved us literally hours of planning".
ramesh31 5y ago
>This should be normal practice IMO. Coding is the process of fully understanding what needs to be built. We've all seen architecture astronauts churn out reams of UML that still result in a broken system. Exploring the space via iterative MVP is far more productive.
- deleted 5y ago
  [deleted]
- jlg23 5y ago
  But when your deployment costs run into the 7 to 10 digit numbers, you might long for better peer review of your code. Formal proofs provide that.
  - zozbot234 5y ago
    The best application for formal proof is actually in lightweight sanity checks as opposed to "deep" review of your code. To put it very clearly, it should simply not be possible for a properly-engineered program to conflate feet w/ meters and crash a space probe as a direct result of that conflation. There's just no way that this is ever valid semantics.
    - p_l 5y ago
      interestingly, that's one of the areas where Ada shines, as you can define your own integer subtype that will help you preserve the semantics (and Ada has, iirc, no implicit casts, so it would require explicit cast to push feet into metres (and it might be made so that such cast would actually convert the values properly)
      - okl 5y ago
        Ada subtypes are "compatible" in that you can implicitly convert them, you're referring to types.
  - actinium226 5y ago

olah_1 5y ago

I'm sure Ada makes a reliable program, but wouldn't it also be good to have an Erlang/Elixir style "self-healing" system with supervisors that can stop and restart each other?

Jtsummers 5y ago
That actually is done with a lot of these kinds of systems. In many of the ones I've worked on you have software or hardware "watchdog timers" that have to be reset, or a process will be terminated and restarted (how will vary a bit). Hardware watchdog timers usually trigger something like a reboot, causing the program to be reloaded and restarted. That's about the simplest you can make a supervisor, but you can have more complex ones monitoring the actual internals to respond should the state become corrupted in some fashion as well. https://en.wikipedia.org/wiki/Watchdog_timer https://en.wikipedia.org/wiki/Watchdog_timer
- trothamel 5y ago
  The programs that ran on the Apollo Guidance Computer were written this way. If there was a sufficiently bad error, the AGC would restart execution. The programs took advantage of the memory in use at the time being non-volatile, and not reset to zero when the computer restarted, so the program could figure out what the CSM or LM was doing, and continue it. This actually happened on Apollo 11. The 1201 and 1202 program alarms were the computer overloading, and running out of space for more processes. When this happened, the computer would reset, and navigation would pick up again.
- touisteur 5y ago
  To add to this, usually most of the systems in avionics or support systems on the ground are dual-hardware (when not more). There's lots of work done to ensure there's no single point of failure and hardware (and more and more, software) failures are handled safely. Regulators add every 5-10y some pressure on time-to-recovery and acceptable data of service loss (counted in milliseconds even on ground systems). Erlang didn't invent much there, and restarting/rebooting isn't always possible (try doing that in less than 10ms). Sometimes, the application itself needs to handle problems. This puts lots of 'classic IT' (interface bonding, fail overs, etc.) stuff to the bin very quick.

mLuby 5y ago

To be clear, they are not currently—nor have they ever—landed on the Moon. better: s/Is Using/Will Use/ best: s/Is Using/Intends to Use/

exdsq 5y ago

Anyone here using ADA? Seems really interesting

rvnx 5y ago
Airbus
nextos 5y ago
Altran / Praxis and AdaCore. Used in the software for e.g. French nuclear power plants and other safety-critical systems.
- touisteur 5y ago
  Hi, do you have a source for the French nuclear plant use? Some kind of paper? Really interested in real-world applications of Spark and had never heard of such. To me the nuclear world was walled off with very specific tech, different than the stuff from rail or avionics.
  - nextos 5y ago
    I've worked on railway systems, but I didn't use Spark. I've seen many mentions to Spark being used in nuclear power software during conferences and presentations. But I'm afraid open materials might not be available... Here you can see some real uses of Spark listed: https://www.cse.chalmers.se/edu/year/2017/course/TDA294_Formal_Methods_for_Software_Development/Lectures/Files/aw_altran_spark_slides_sept_2017.pdf https://www.cse.chalmers.se/edu/year/2017/course/TDA294_Form...
    - touisteur 5y ago
      Thanks! I know of some rail projects in spark some colleagues worked on (and some internal company recruiting efforts) but I guess it's quite recent and maybe not yet deployed. I'll ask around about nuclear, thanks again!
VygmraMGVl 5y ago

dandotway 5y ago

Ada's formal verification capabilities have fallen behind Frama-C for ANSI/ISO C. Frama-C allows formal verification of essentially arbitrary heap manipulation algorithms. You can implement linked lists and graphs in traditional C with Frama-C annotations in the comments, then prove your code never dereferences NULL, never has an integer overflow, etc. One single commercial Ada vendor offers Spark, a formally verifiable subset of Ada. Spark does not allow arbitrary dynamically allocated data structures like Frama-C does. https://frama-c.com/ https://frama-c.com/

p_l 5y ago
Seems that's no longer true, as current SPARK version permits pointers given they follow certain memory ownership policy.
- dandotway 5y ago
  Yes, SPARK has a Rust-like borrow checker that doesn't allow implementing arbitrary pointer graphs. You have to use 'unsafe Rust' to implement linked list containers which, once implemented, other parts of the codebase can then consume in 'safe Rust'. Seems to be the same deal with SPARK ('safe Ada') vs vanilla Ada ('unsafe Ada').
  - p_l 5y ago
    Interestingly both Frama-C and SPARK use linked list as an example. But yes, not everything can be verified, though I'd rather bet on Ada than Rust in this area.
    - dandotway 5y ago
      The SPARK example I found uses singly-linked lists and says doubly-linked lists and graphs with cycles are not supported: https://blog.adacore.com/pointer-based-data-structures-in-spark https://blog.adacore.com/pointer-based-data-structures-in-sp... Yes, I could and should have been more explicit when I spoke of 'linked lists' without further qualification. While talking about these languages designed to eliminate all ambiguity I would do well to be unambiguous. :-)

smoyer 5y ago

Just a small gripe - this article shouldn't really be "How Masten Space ..." I think that story would be fascinating. This article is more of "Why" and "What" which is still worth reading.

bpodgursky 5y ago

Headline might want to indicate it's SPARK, not Spark (the Hadoop-ecosystem project). As someone with a lot of experience building systems in the big data space... I was very concerned for their lander.

deleted 5y ago

[deleted]