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

https://www.adacore.com/uploads/techPapers/Masten-case-study.pdf

88 52 5 years 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• 5 years ago

What language is GNAT Studio written in?

exdsq3• 5 years ago

Ada lol - think I see what you’re getting at there. GTK toolkit and python as an internal scripting language.

okl2• 5 years ago

Ghosh says they’re trying to fully understand what they’re building before they start coding.

This should be normal practice IMO.

sjburt• 5 years ago

I've seen this approach. The wrong thing still gets built, but at least you know why it was built that way.

mhh__• 5 years ago

"Thinking doesn't guarantee that we won't make mistakes. But not thinking guarantees that we will" - Leslie Lamport

ramesh31• 5 years 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.

jlg23• 5 years 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.

kjs3• 5 years ago

"Move fast and break things...in SPACE". That doesn't sound like the process I'm looking for in such things.

KronisLV2• 5 years ago

Coding is the process of fully understanding what needs to be built.

Not every domain affords you the luxury of coding the wrong thing and then fixing it in a later iteration. Sometimes due to financial constraints, other times because people wouldn't exactly be okay with the 0.7.1 version of your plane software leading to crashes until the next patch.

That said, i somewhat agree with you that UML and abstractions can only lead to problems if there's too many of them. A few high level overview diagrams can be good to have, but only as long as they conform to the actual architecture and models 1:1, and as long as they're not made at the expense of actually writing working software and perfecting it.

However, as long as only one person with incomplete knowledge of the domain or requirements is the one to write the code, you'll still end up with sub par solution. Personally, i think that the only way around that would be a paradigm shift of sorts - instead of planning meetings that aren't good enough, you might as well do programming meetings and mob programming in which you'd code the most important architectural bits of the software that you need, leaving the legwork for individual contributors later.

In my experience, code review is far too late for serious decisions to be made. At best, the reviewer will need to wrangle with hammering your sub optimal code into shape, at worst they'll just be like: "Sure, this looks like Java, it can go into the main branch. QA can figure out whether it's good enough or not."

eptcyka• 5 years ago

If you're exploring the space via an MVP, then you cleaely do not yet fully understand what needs to be built.

olah_1• 5 years 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• 5 years 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

trothamel• 5 years 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.

touisteur6• 5 years 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.

SkyMarshal• 5 years ago

Ada/Spark can do that too, but you also want things like memory safety, hard real-time and/or constant-time capability, and provable correctness. Ada also enables those capabilities.

Verdex• 5 years ago

I'm interested in hearing more.

I've been looking into erlang on and off for nearly 14 years now. I think the language is really neat. But the self-healing supervisor tree thing is something that I've yet to get my head wrapped around.

Like ... if you have some code that's like "X / 0" then it seems like it's not going to matter how many times you restart the process.

macintux• 5 years ago

The general strategy is to test the system to the point where any bug like that is an edge case, some weird input you didn’t expect.

So every time you get that input you’ll still crash, but other transactions will continue normally. Hopefully that input is either due to a transitory glitch like a bit flipped in RAM, or a user who isn’t bored enough to keep submitting it, but either way the process isolation means all your other jobs can continue.

MaxBarraclough• 5 years ago

I'm not sure that mindset fits for this kind of problem. It's not a web server handling lots of independent requests, it's a real-time critical system that is required to always transition to the correct state within the deadline. I'm no expert on this stuff though.

mLuby• 5 years 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/

exdsq3• 5 years ago

Anyone here using ADA? Seems really interesting

rvnx• 5 years ago

Airbus

nextos2• 5 years ago

Altran / Praxis and AdaCore.

Used in the software for e.g. French nuclear power plants and other safety-critical systems.

touisteur6• 5 years 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.

VygmraMGVl• 5 years ago

I've heard BAE uses ADA on their satellites.

touisteur6• 5 years ago

Most air traffic management radars.

KronisLV2• 5 years ago

Took a university course on it way back. Seemed about as pleasant to use as Pascal, though the ecosystem around ADA felt non existent. Probably better to use it for lower level logic when stability and correctness are the primary concerns.

On the bright side, at least there's an open source compiler available for it as a part of the GNU project: http://www.gnu.org/software/gnat/

Here's a quick intro to the actual language: https://learn.adacore.com/courses/intro-to-ada/index.html

int_19h• 5 years ago

Note that Ada is not an acronym - it's a person's name.

(Also, confusingly, SPARK was originally an acronym, but isn't anymore - yet it's still written in all-caps.)

butterisgood2• 5 years ago

It's just Ada, not the Americans with Disabilities Act (ADA) or the American Dodgeball Association or whatever else it is.

Ada is just a name, like Ada Lovelace, its namesake.

exdsq3• 5 years ago

I have autocorrect because I worked on a cryptocurrency that’s coin was ADA so I need to manually change it

dandotway5• 5 years 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/

p_l3• 5 years ago

Seems that's no longer true, as current SPARK version permits pointers given they follow certain memory ownership policy.

dandotway5• 5 years 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').

rurban• 5 years ago

With CBMC it's even easier. You don't need magic comments in foreign languages to prove linked lists, arrays, graphs, trees, hashtables, ... If you need to formalize contracts you do it in C, but rarely need it

http://www.cprover.org/cbmc/

touisteur6• 5 years ago

Strange (but interesting (point of view. I always found Frama-C so verbose where spark has most checks as implicit, and has ways to express not-null pointer as types. I've always found eacsl a pain to write and even more with pointer manipulation.

Spark has added checks on memory ownership, that it seems (willing to be corrected) Frama-C didn't have yet.

From a pure tech stack point of view, down there you'll find Why3 and SMT solvers to perform most automatic proof/discharging of verification conditions, and then around that you'll find either a rich set of plugins (Frama-C) because C is... a tall order, or a series of static analysis tools (heavy-duty like codepeer, or lightweight libadalang-based abstract interpretation things) combined into the proof and verification environment. There's also been a lot of amazing work on floating point code verification for both in the previous years, and it was done mostly at the Why3 and SMT solver (or different kind of solvers/verifiers such as gappa) so everyone profits.

And, lest people might think both communities don't interact, the Spark and Frama-C people have an annual (or is it every other year) joint conference.

I'd be quite happy to find more people diving into Frama-C and see what they do and how they manage to write safe software. I'd also be quite happy to see rust building over Why3 (among other things) for their proof/verification efforts. More fruits from all the deep efforts of the verification community.

dandotway5• 5 years ago

Responding to each point you raised:

'Frama-C so verbose': ??? Ada is the most verbose programming language, ever, even before you had the extremely verbose Spark contracts. Could you show me an example of Frama-C with annotations being more verbose than Ada/Spark?

'Spark has added checks on memory ownership': A Rust-like pointer ownership tester has its advantages and limitations.

Advantages: if you have team of 20 engineers working on a 20 million line web browser and no single engineer understands how the whole code base works, a pointer borrow-checker prevents an important class of errors.

Disadvantages: Rust tutorials point out that you have to resort to 'unsafe Rust' to implement even an intro-to-computer-science linked list. You have to use unsafe Rust to implement your fancy heap manipulation algorithms. Unsafe vs safe Rust is a bit like Ada vs. Spark ("safe Ada").

'I'd be quite happy to find more people diving into Frama-C': Frama-C is trending upward and Ada is in decline, ever since the Ariane 5 explosion on 4 June 1996. The US DOD consequently shut down its Ada office and eliminated the Ada requirement, and C/C++ subsets increasingly dominated.

philwise• 5 years ago

Are there vendors who provide support for tool qualification for frama-c? By that I mean documentation support that can be provided as part of the certification process, so when you say "Frama-c verified this code does not contain any arithmetic overflow", it is possible to back that up with "And Frama-c version x.y.z has sound analysis, evidenced by ...."

dandotway5• 5 years ago

Great question. C/C++ is definitely trending upward in 'safe software' systems even though it isn't ready and industry as a whole isn't (as far as I know) using Frama-C. Are Tesla/Google/Apple hiring Ada engineers to build the car autopilots that control whether we live or die? Nope, seems to all be C++, God help us all.

smoyer• 5 years 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• 5 years 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.

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

Related Stories