top | item 3943556

What's The Best Language For Safety Critical Software?

109 points| pooriaazimi | 14 years ago |stackoverflow.com | reply

116 comments

order
[+] _djo_|14 years ago|reply
The Integrated Navigation and Weapons System (INWS) developed by ATE Aerospace for the Hawk Mk.120 was written entirely in C, was DO-178B-certified, ran to a million lines of code and cost approximately $100 million for the development of the software and hardware combined.

The software includes integration all the standard military navigation and weapons targeting and control functionality, along with a secure datalink using the Link-ZA protocol and a nifty radar simulation system (basically an airborne LAN for air-to-air training) that runs over it.

They just delivered the latest iteration of the software which allows them to receive data-linked air picture information from other aircraft, such as an AWACS platform. Throughout all this the project has had no major snags, has missed no deadlines and has come in on budget.

So my point being that it's possible to write complex safety-critical software in C if your processes and programmers are good enough and you're willing to pay about $100 million for it.

[+] derefr|14 years ago|reply
Emphasis especially here:

> if your processes ... are good enough

I would say that it's possible to write complex safety-critical software in any language, provided it's completely specified beforehand in, well, military detail. This program was likely done when that spec hit the programmers' desks--the project from that point on basically consisted of transforming pseudocode to language-of-choice-X without mucking anything up in the process.

[+] ajross|14 years ago|reply
You don't need to look that far afield. Literally everything runs over a kernel written in C.

But that being said: this is just proof that it "can" be done, not that there aren't better choices. Specifically, could you do a missile management system in less than a million lines of code or for less than $100M with equivalent performance and quality on another platform? I think most of our intuitions would agree that you could.

[+] masklinn|14 years ago|reply
> It is a functional language, which means that code has no side effects. This property of declarative languages in general and pure functional programming in particular means that the program can be assumed to do exactly what it says on the tin and no more. The absence of side effects makes it possible to do a formal correctness proof of the program because the program code describes the whole computation. This assumption cannot be made with imperative languages such as C.

As much as I love Erlang, nothing in this paragraph applies to it (it would apply much, much better to Haskell though still not perfectly): Erlang is not a pure language and it does not put any limitation on side-effects (the way Haskell does by putting them in separate monadic containers unless an `unsafe` function is used).

Erlang does use immutability (its only mutable data structure is the process dictionary[-1]), it does not share state between concurrent processes[0] and features pattern-matched bindings (technically `=` in Erlang performs pattern-matching, not equality, but if a matchable part is unbound Erlang will simply fill it with the correspondence from the other side, as a result it behaves much like single assignment in many situations), which do help in making code pure and correct, but fundamentally its approach to reliability is not to make code unbreakable (the way you'd do by formally proving it for instance) but by making recovery and error management easy, simple and widely supported by the runtime and its libraries (OTP), in (no small part) part by applying the telecom-borne principles of separating concerns (between the thing that does the job and the thing which recovers the error in case the first one blows up) and building redundant systems (if you have a single machine and it crashes you're gone, if you have 2 machines and the first one crashes the second one can handle things until the first one comes back (and you can have a third machine overseeing that with its own hot spare), Erlang encourages doing that at the process level)

[-1] a process mailbox might also be considered mutable, in a way

[0] it does share memory for big binaries — they are shared and reference-counted — but these binaries are immutable so no state

[+] tel|14 years ago|reply
I think the dialogue is starting to see functional as a positive thing but now that the distinction between "purely functional" and "has first order functions" is becoming increasingly important, the effort previously put in place to blur it is backfiring.
[+] pooriaazimi|14 years ago|reply
(Can I post a completely irrelevant comment about something that just baffled me? I submitted this question 40 minutes ago. Now I went to StackOverflow and it just awarded me the gold badge of 'Publicist', meaning that this link has been visited by 1000 unique IP addresses! I had this question open in another tab and it's true: it had 4950 views (with the best answer having 90 up-votes) when I submitted it, and now it has more than 6450 (best answer: 115 votes)! I honestly didn't know there were so many HNers... I always thought HN was a relatively small community.)

Sorry if it's not relevant, but I thought it might be interesting to others.

[+] sp332|14 years ago|reply
Yeah I thought the number of commenters was a reasonable approximation of the number of users on the site. I also was shocked when I found out how many people are on here! Turns out I'm an outlier in terms of commenting (I'm actually #76 https://news.ycombinator.com/leaders ).
[+] gregholmberg|14 years ago|reply
Task: write a static analyzer to check primary control software for a new family of passenger airliners. [1]

Employer: Airbus.

Which language did the team choose for the analyzer? OCaml.

It is possible to write OCaml programs that are provably correct.

[0] "Caml language family" http://caml.inria.fr/

[1] "Success Stories" http://caml.inria.fr/about/successes.en.html

[2] "OCaml: a serious contender" http://caml.inria.fr/about/programming-contest.en.html

edit: clarity

[+] pgroves|14 years ago|reply
It's worth pointing out that Airbus has a large presence in France and Ocaml is from a French research institution (INRIA). I highly doubt that's a coincidence.

Disclosure: Ocaml is my favorite language by far.

[+] tjr|14 years ago|reply
What language was the primary control software written in?
[+] Nelson69|14 years ago|reply
This very question scares the hell out of me. Language just seems so far away from what really matters.

The language is a part of this, but assembling the right team with the right mentality is the key. There was the DOD Ada mandate and over the years there were some interesting studies showing reliability differences between Ada and C++, but also in hopes of keeping costs lower, they use C and C++ in a lot of that stuff now so that they can use off the shelf software libraries and such. That says a lot, the ability to hire people and develop with some velocity matters too. Language won't make a shitty architecture good. Language won't make a shitty team good, either.

Fundamentally, if you pay attention to where this stuff matters most, Ada has to be a standout choice but those industries don't change, they don't adopt new stuff and the whole process by which that happens in them isn't one that results in the best technology, it's one that results in a consensus technology. The risk of a line of code knocking a plane down or letting the missile hit the wrong target are just fundamentally different than letting someone log in to a web site; maybe they shouldn't be but the very culture difference between those groups is huge and so you can look at them and say "ah, we should use Ada too, 'it's safer'" but that is probably not a great business decision. At least, not right now.

[+] dkersten|14 years ago|reply
I don't think anyone cares so much which languages you use as long as everything is certified. Since certification costs a ton of money, people would generally use languages which already have certified compilers, runtimes, libraries, tools, OSes etc as it would be cheaper than getting a different language toolchain certified. This seems to mean C and maybe still some Ada.
[+] oggy|14 years ago|reply
I do some work on formal verification, so I can talk about it from that perspective. Purely functional code is the easiest to reason about, but then again you a) can't interact with the "real world" in pure code, and b) "safety critical" often goes hand in hand with "embedded" and "low-level", where you usually don't want to lug a runtime around. So you will probably end up with an imperative language of some sort or the other.

In such a case, the programming languages and programming practices which facilitate formal reasoning are more or less the same ones which facilitate informal reasoning. Avoid "spooky action at a distance", i.e. keep state changes localized (this enables you to use, say, separation logics). Funky flow control is difficult to model/reason about. Non-determinism as well. Type safety and static type systems help.

Then again, if "safety" includes "security", you not only have to wonder whether your system is correctly implementing its API, but also whether the API is secure in itself. A paper by Steel & al [1] contains a partly amusing, and partly frightening account of one such investigation.

[1]: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFS-ccs10.pd...

[+] protomyth|14 years ago|reply
Even though I am not a fan, Ada seems to be a good choice for this sort of thing. People have years of experience, the language design pushes towards safety, and the compilers are well optimized.
[+] jvanenk|14 years ago|reply
My experience in aerospace has been that people still distrust optimizers. Generally, they are turned off. Same thing for things like CPU cache.

Not exactly relevant to this discussion, but good to keep in mind.

[+] kamaal|14 years ago|reply
From one of the comments.

---

NOTE ON JAVA SUPPORT. THE SOFTWARE PRODUCT MAY CONTAIN SUPPORT FOR PROGRAMS WRITTEN IN JAVA. JAVA TECHNOLOGY IS NOT FAULT TOLERANT AND IS NOT DESIGNED, MANUFACTURED, OR INTENDED FOR USE OR RESALE AS ON-LINE CONTROL EQUIPMENT IN HAZARDOUS ENVIRONMENTS REQUIRING FAIL-SAFE PERFORMANCE, SUCH AS IN THE OPERATION OF NUCLEAR FACILITIES, AIRCRAFT NAVIGATION OR COMMUNICATION SYSTEMS, AIR TRAFFIC CONTROL, DIRECT LIFE SUPPORT MACHINES, OR WEAPONS SYSTEMS, IN WHICH THE FAILURE OF JAVA TECHNOLOGY COULD LEAD DIRECTLY TO DEATH, PERSONAL INJURY, OR SEVERE PHYSICAL OR ENVIRONMENTAL DAMAGE.

---

Made me smile and also scared me at the same time.

[+] huherto|14 years ago|reply
Just trying to avoid a lawsuit.
[+] kitsune_|14 years ago|reply
I had to learn Eiffel at college because my prof was its inventor (Disclaimer: I really have a problem with this way of 'teaching'). And as such it was bolted into our brains, that in software engineering, it just so happens that everything that Eiffel 'solves', is precisely what is 'amiss' in other languages. I was mainly pissed that besides Prolog, I had to learn yet another obscure language.

In hindsight, I do think I might have been a bit judgmental back then, Eiffel has some very nice constructs and language limitations that allow you to build safety critical software (as you put it).

[+] bob_kelso|14 years ago|reply
A similar thing happened to me. Our professor forced us to program a lot in a language of his own invention called Morpho (http://morpho.cs.hi.is/). Although it does have some cool features I don't think anyone has ever written anything properly useful in that language and I'm fairly certain that I will never ever write another line of Morpho in my life. I'd say you were lucky since Eiffel is actually used to some extent out there in the real world.

There should be some sort of ban or restriction for teachers teaching their own textbooks or obscure languages.

[+] kaolinite|14 years ago|reply
I've found that software written in C is often the best written and most stable software I've used. I believe it's due to the amount of care required in writing in the language and the fact you can't stream code out as fast as you can in other, 'safer' languages. Overall though, I think the most important thing is to have skilled developers who understand the tools, libraries and languages that they're using.
[+] jvanenk|14 years ago|reply
> Overall though, I think the most important thing is to have skilled developers who understand the tools, libraries and languages that they're using.

I work with C every day as an embedded developer. I've done a lot of safety critical work. By far the worst aspect of safety critical development is the complete inadequacy of many programmers who work on it.

The level of complexity that shows up in these system scares me. Even when introducing languages like Ada, people find a way to abuse them. Budgets get tight, schedules slip, and verification gets lax. These programmers are then the only people capable of dealing with the massively complex system they've built and the cycle repeats itself.

Ada's a great language, but it's not a panacea. I'm working on a language for embedded systems as well, but it's not going to ever fix the 'bad programmer' problem. The best I can hope to do is find ways to reduce the complexity of these systems through language features.

[+] pooriaazimi|14 years ago|reply
Very true.

But in some cases, you simply can't use something like C. A friend of mine is currently trying to write a microkernel and mathematically prove that it's 100% bug-free (similar works on the L4 microkernel: [1] and [2], though they might not be the best articles on this matter as I just found these links with a quick Google search). He uses Haskell and ML for this project (He'd use Ada, but he already knows some Haskell and ML and doesn't want to re-learn everything).

[1]: http://ertos.nicta.com.au/research/l4.verified/

[2]: http://www.linuxfordevices.com/c/a/News/NICTA-sel4-OK-Labs-O...

[+] tseabrooks|14 years ago|reply
The article points out great benefits of using C in safety critical systems. However, as an embedded dev for 5 years... I'd say the advantage is the same as the disadvantage. Nitty gritty bit level memory manipulation and management can be excellent. However, C may also take your measure and find you wanting. In this case the resulting code will be a disaster. I've written both disastrous code and then grew and wrote some great code in C.
[+] gm|14 years ago|reply
And yet we have ANOTHER extremely good programming question with really great replies, which asshole moderators have closed on StackOverflow. This one as "not constructive".

The one thing that fucks up SO is the moderators.

[+] ceejayoz|14 years ago|reply
It's open again.

I'd like to see an increasing threshold for closing once reopened. Something along the lines of if reopened once, 10 close votes required... if reopened twice, 20 close votes required.

[+] npsimons|14 years ago|reply
Coming from someone who's done embedded work (although nothing that's controlled an airframe), I have to say that methodology is much more important than language choice. Sure, choosing something that is deterministic and that you have half a chance of Proving Correct can help, but you're probably better off studying CMMI or Zero-Defect Software design[1]. Just as reference, the JSF (F-35) software is being written in C++ by the DoD, although that group is one of the few CMMI level 5 groups in existence. While I personally hate CMMI, I have to admit that it is one way to ensure an organization is accountable and ticking all the checkboxes.

That being said, avoid PHP, Matlab and C# at all costs if safety is at all important to you.

[1] - http://www.amazon.com/Toward-Defect-Programming-Allan-Stavel...

[+] josefonseca|14 years ago|reply
"What's the best language" is a sure fire way to not get any useful answers(because you'll get all possible answers) from a crowd of programmers, IMO.

What's "best" for what? Does the safety critical system need to be fast and respond to real time events in real time? Or is it safety critical but is allowed to be slow? What kind of hardware is it running on?

Depending on your hardware, the only safety critical language may be assembler, so you can check every single instruction and make sure it's precise.

Having said all that, Apollo 11's code was written in a meta-language, then compiled to assembly instructions, then hand-compiled into computer code. You don't get any more safety critical than taking the first men to the moon.

http://googlecode.blogspot.com.br/2009/07/apollo-11-missions...

[+] vbtemp|14 years ago|reply
I'm not an expert on Apollo flight software, but comparing the role of flight software in the avionics of 60s era spacecraft isn't really a fair comparison. From what I recall there were a number of FSW faults and overloads just prior to the lunar landing, which had to be manually (literally flipping a switch) reset and overridden. Today software is the "complexity sponge" of most aerospace systems - I recall some figure that in the F-4 (a 60's era figher), about 4% of moving surfaces were under software control. These days on contemporary fighter jets and spacecraft that figure is in the 90% range.
[+] Czarnian|14 years ago|reply
Safety-critical software is any software where failure can result in death/severe injury to a person or loss/severe damage to equipment/property.

There are concrete answers to the question. Many languages are just flat not capable of being safety-critical.

[+] SteveJS|14 years ago|reply
Making the front page on HN is a sure fire way to get a SO question closed.
[+] jsdalton|14 years ago|reply
I was just about to make that observation myself.

This question has been around since 2008 and clearly has garnered enough interest to earn 167 votes on its top answer. It's definitely one of those question/answers that I walk away feeling more knowledgable from -- and presumably the people upvoting it on HN feel the same way.

So yeah it survives intact and unmolested for nearly 5 years -- but an hour on the HN front page is its death knell.

I guess I understand the reasoning behind closing it, but it smacks of the worst kind of pedantry.

[+] vbtemp|14 years ago|reply
I've seen some pretty phenomenal flight software written in C. Well-architected, solidly implemented.

I've also seen some pretty horrible flight software written in C.

Naturally, and as with all software, clear requirements, avoidance of "feature creep", and a clear vision of the lead developers is what distinguishes the good from the bad. So these are critical components of "safe" software development, irrespective of whatever "safe" language you're using...

Edit: On second thought, strict adherence to a uniform coding standard is incredibly important too. Even though it's just cosmetic, it holds the developers to a higher standard, and strongly discourages breaking the rules to get things done quickly.

[+] Arcticus|14 years ago|reply
Safety Critical software is really about the confidence level in the software to function as intended and is really language agnostic. This is why most Safety Critical projects focus on development and test practices. You want to have a good warm and fuzzy that the product your outputting will work as intended when needed. The traditional way to accomplish this is through rigorous design processes and robust testing. So no one language has an advantage over another (unless real-time is a requirement which it often is) at the root level. Over the years tools have been developed to help assist in testing and giving you that warm fuzzy feeling at the end. Static analysis tools and code coverage tools are an example. These tools tend to be more mature for traditional languages like C/C++ and ADA thus making them more popular for Safety Critical projects, but that's not to say another language that the development group was more familiar with wouldn't do better. At the end of the day its all about your ability to detect defects and the systems ability to detect anomalies so the tool set that the development team thinks they can accomplish this the best with is the best choice.
[+] nobby-w|14 years ago|reply
I actually wrote that posting and I'm wondering about the formal verification of Erlang now. My understanding is that you could formally reason about Erlang systems if you adhered to coding standards that allowed this, and formal proofs had been used for at least some of the code base on the AXD301.

I'll quite happily edit that out of the answer if I'm wrong. Can somebody elucidate this here - Am I barking up the wrong tree about verifying Erlang systems?

[+] spitfire|14 years ago|reply
Currently, Ada. It's a fair tradeoff between formal verifiability and time/space control. You have to do a lot more extra work to meet these three requirements.

In the future, as we figure out how to make things like Haskell or an ML meet all three requirements, we'll move away from the labour intensive languages.

In fact, if strict real-time requirements aren't necessary Haskell is already useful. It's being used in the UK's national air traffic system.

[+] cpeterso|14 years ago|reply
I think Haskell's lazy evaluation may make more difficult to verify formally because execution time and memory usage are less predictable.
[+] bklbkl|14 years ago|reply
The UK's national air traffic system used ADA, not haskell.
[+] jpro|14 years ago|reply
Let's not forget that Fortran is used in many of the world's Nuclear power plants