What's The Best Language For Safety Critical Software? | Hacker News Reader

What's The Best Language For Safety Critical Software?

stackoverflow.com

109 pointspooriaazimi116 comments

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.

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.

Literally?

Meaningless semantic quibble. Yes, "literally" everything. Or everything worth talking about anyway. Do you have a counter example of a complete system seeing active development in the modern world without any use of C at all? I certainly can't think of one.

Of course, many micros are still programmed in assembly. And assembly still plays a big part in many subsystems, though I would concede much would be written in C. Not literally everything.

I'm aware of no microcontroller work in the modern world that is done solely in machine code. Again, you have a counterexample?

I write assembly for microcontrollers constantly. If you require reliable timing at the cycle level, you have absolutely no choice in the matter.

Sure. But you don't write a system only in assembly. The point, now buried in this silly thread, was alexchamberlain's nit that it wasn't "literally" true that all systems are built on top of C kernels (whether it be an OS kernel, firmware, whatever).

You can call me what you like and if you'd said "everything" instead of "literally everything", I would have let it slide. You were being quite misleading.

Given that you haven't provided a single counterexample, I can't see how I'm being misleading. All modern systems are built on C. All of them.

And for the record, I didn't call you anything. A "nit" is a pedantic correction, c.f "nitpicking". I could have said "quibble" too. It's a reference to your words, not you.

But having C with all its vulnerabilities in the kernel caused many - if not most - of the security relevant issues of the kernel(s). Think of buffer overflows alone.

As far as I'm aware, a lot of the safety critical certification requires the entire stack to be certified, in which case the OS (which would probably be a hard-realtime OS) would be certified too.

Probably part of the $100M price tag is a hefty license fee to use said OS.

Yep, unfortunately I don't know which OS they went for but it was one of the commercially-available RTOSes on the market. Those don't come cheap.

Avionics software certification is phenomenally expensive. Both Airbus and Boeing have warned in recent years that it has become such a big part of their development costs that they're concerned about it becoming unsustainable.

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.

Not all languages lend themselves to formal certification, which is why such mission-critical software is typically written only in C, C++ or Ada.

And while the specification process is obviously extremely extensive, it's only a part of the total process and not a guarantee of bug-free code. Many of these projects have gone pear-shaped during the implementation phase despite having good specifications.

So that's why having good programmers, a good development process, solid libraries and great tooling is so important for the implementation phase. Especially because the requirements always change during development, even for mission-critical military avionics software.

One of the main problems with the F-35 program is that the implementation phase for the development of the plane's software has gone badly wrong. It's already by far the most expensive avionics program ever.

Finally the testing phase is super-critical. ATE designed their own extremely thorough testing setup, ranging from software verifiers to full-scale test-benches to simulate on the ground the full range of software functionality in flight.

It's a difficult process that's very easy to get wrong as a result of the incredible complexity of modern avionics and weapons systems. I am in awe of those teams that get it right.

There is nothing about C or C++ which would make programs written in these languages especially suitable for formal verification.

You could argue the one language which actually does lend itself to formal verification is the one which has been formally specified via operational semantics; namely, Standard ML.

There is one thing that helps about C and C++. In a safety-critical system, the entire runtime has to be certified. This isn't a problem for C and C++ because their runtimes are very minimal. DO-178b Level A-certified implementations of the standard libraries exist for various real-time operating systems. As long as you use them, you're golden.

However, any system that runs on top of a virtual machine is problematic because of how extensive their runtimes are. Developing an efficient and competitive DO-178b-certified JVM, for example, would be a huge undertaking, but so would modifying an existing JVM.

Further, anything garbage collected is a problem because you can't have any situations where a timing constraint is violated because of your garbage collector. The best way to prevent this would be to schedule, say, 50 milliseconds every second for garbage collection. But there's still a limit there where the GC can no longer keep up with the rate of garbage production, which could lead to your application running out of memory and failing. Proving that your application will never reach said limit would be hard either by static or dynamic analysis.

I actually once worked on a safety critical military application (though not DO-178b certified), and for a new version, we switched from C to real-time Java (RTSJ). RTSJ actually let's you avoid unpredictable GC altogether through what is called "scoped memory" in your critical threads, and provides real-time scheduling if run on a RTOS.

We switched because we wanted to reduce the risks of bugs, but you must remember that in most mission critical applications, one must consider failure not only in the software. You use redundancy - in the software, in the hardware, and in the network. We even used several separate power systems and several redundant generators.

Interesting, thanks! I didn't know about RTSJ and a cursory search in preparing my earlier comment only popped up links that looked bitrotted, so I assumed it wasn't a widespread technology.

It isn't widespread. Then again, hard real-time systems aren't widespread either. I think Boeing was (maybe still is) using RTSJ. The only downside it has is increased RAM footprint relative to C(which makes it unsuitable for very limited devices) and a small performance hit relative to regular Java because some classes need to be compiled to machine language ahead of time (the Hotspot JIT can do some very nifty optimization at runtime, but those come at a cost of non-determinism. Real-time systems always trade performance for determinism).

EDIT: see http://goedel.cs.uiowa.edu/MVD/talks/Vitek.pdf presentation slides from 9/2012 on realtime and safety-critical Java.

That's exactly the reason why C, C++ and Ada continue to be the primary choices.

There are a few interesting developments regarding Java for safety-critical and mission-critical applications. One is JSR-302, which is defining a safety-critical subset of Java which will not have garbage collection and will use of a run-time stack rather than a heap for temporary object allocation, the removal of dynamic class-loading, changes to task scheduling and a smaller standard library. These should make it possible to certify JSR-302-compatible Java runtimes and applications for safety-critical and mission-critical tasks.

The second is DO-178C, the follow-on to DO-178B, which will incorporate additional work on the certification of object-oriented languages such as Java.

I agree. It depends on what subset of C and C++ is used. If macros are used the only way to actually verify the code will be to pre-process it. Worse is if templates are used. Some templates don't even finish compiling.

http://cpptruths.blogspot.com/2005/11/c-templates-are-turing...

Most likely no one will write such a template in a mission critical system. However, from a formal verification standpoint the only way to verify the code is to check the binaries.

> 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

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.

Well it is true that ("sequential") Erlang is a functional language. It was built as a functional language and has pretty much all the features usually associated with functional languages. It does not just "have first-class functions".

But it is important to understand what "pure" is and is not, that almost no language is pure (because it's hard to produce useful pure software, or even to define how it would work precisely) and that very few strongly encourage purity (at the language level, many do as a social level but offer no help or support for actually doing it when writing code)

"functional" should never have meant "has first-class functions" to anyone.

I agree, but it was often marketed that way.

That's exactly what functional means. You're conflating functional and pure. They happen to be (essentially) the same thing in Haskell, but that's not always the case. A functional language can get you really close to pure (but good luck doing anything interesting without monads or mutable state), but even the purest languages cheat. Putting your side-effect code in a main function might help you catch bugs and limit potential side-effects, but it's still not completely pure (and for good reason, at the end of the day you actually want to do stuff).

"Pure" is an adjective applied to "functional" so I don't see the conflation as odd. A language like JavaScript has first class functions, so it's a little bit functional. But no more than that, because most expressions aren't (mathematical) functions. Haskell is purely functional because everything's a function. (I/O primitives like getChar excepted, etc., etc.)

Meanwhile, languages like Haskell don't cheat quite as much as you suggest. Monads are functions, and even in the IO Monad you're doing purely functional manipulation of IO primitives. Think of it as a purely functional funnel through which the dirty data of reality is poured.

He knows what it means. That's why there is a 'should' in that sentence. GP indicates that using functional in this manner is a poor choice.

That's actually what "functional programming" means. https://en.wikipedia.org/wiki/Functional_programming

Read your article. That's not at all what it's supposed to mean. A functional programming language is one which uses the λ-calculus as its base model of computation. PHP has first-class functions. PHP is not a functional language.

From the first paragraph: Many functional programming languages can be viewed as elaborations on the lambda calculus. Most functional languages happen to be variations on λ-calculus, but it's not part of the definition.

Also, it's possible to write PHP in functional style, it's just not common. http://www.michielovertoom.com/software/functional-php/

Ah, selective quoting:

In computer science, functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids state and mutable data. It emphasizes the application of functions, in contrast to the imperative programming style, which emphasizes changes in state.

All programming languages can be written in a functional style. I can create new function types in C++ with templates and function pointers to simulate the action of closures. A functional programming languages is one which has the λ-calculus as its base model of computation as idiomatic in the language. Note that the description above is exactly what is meant by "λ-calculus as the base model of computation." What the article is trying to say is that some languages can be described almost entirely as syntactic sugar on λ-calculus (or System Fω in certain cases).

You do understand that I can simulate first-class functions in any mainstream language? This is not what PL researchers mean when they say "functional programming." Functional programming languages are those which are also predominantly used in a functional style.

And yet it has among experts and textbook authors for nigh-on 60 years. It's even sometimes presented (quite credibly, imo) as the feature which makes all the other aspects of functional languages worthwhile.

I didn't notice purity become quite the deal it's become until recently, when boosters started talking it up as a concurrency panacea. Sure it's always been ubiquitous, and mutability was seen as a tricky tool that's best used sparingly, but that was seen as a matter of culture as much as it was a matter of definition. Valuing immutability definitely wasn't presented as functional 'territory' - a somewhat difficult position to hold given things like the PURE keyword in Fortran, or the variable and constant keywords in Ada.

> It's even sometimes presented (quite credibly, imo) as the feature which makes all the other aspects of functional languages worthwhile.

In other words it doesn't matter how we define "function" as long as they are first class? that's nonsense.

Regardless of historical (ab)usage "functional programming" should be re-appropriated to mean (from wikipedia): "a programming paradigm based on mathematical functions rather than changes in variable states".

Functions are from math, and mathematical functions are first of all pure (f(x) = x + 1 shouldn't also give your dog a bath).

It's pleasant to think of how far we've come, that now most people can just take it for granted that they can pass around functions, that functions can be anonymous, and that closures work more or less the way they ought to. The only languages I can think of that don't support this stuff are ones that are old (like C), or low-level on purpose (again, like C), or defined by a community that is chronically hidebound (like Java). There seems to be a loose consensus among successful programming language makers that higher-order functions and closures are reasonable and expected.

In the future, I expect the next things to become mainstream from the Weird FP Languages will be more type inference, and side-effect annotations. I've often wished that I could declare a few types in a language where you normally omit them, and have the compiler infer as much from those declarations as it reasonably can. I know it's possible, because the SBCL compiler for Common Lisp already does it. This gives many of the same benefits as stricter typing, but in a very lightweight way. And the idea of side-effect annotation is that you can declare whether or not functions have side-effects, and then have the compiler warn you if your code breaks that assumption -- like the PURE functions in Fortran you mentioned. Considering the dangers of mutable state, anything easy you can do to help keep it straight is probably a win.

(Note that in a sufficiently extensible language, e.g. Arc, these things can easily exist outside the language core. I hope that this kind of extensibility becomes mainstream, but wouldn't get my hopes up.)

We should probably start calling "purely functional" code "referentially transparent" code to help avoid confusion.

Also, I think you mean "first class functions" rather than "first order".

(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.

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 ).

I think the number of commenters fell quite dramatically after they stopped showing the score on comments. Before that HN felt like a much larger community.

When was that exactly? I've been around for about a year and half, and vaguely remember it. I think it was about a year ago. Is it right or my poor memory is playing tricks on me?

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

What language was the primary control software written in?

" ... a subset of the C programming language".

Er, I missed that footnote. Thanks.

I think you found the punch line.

Something like "if you want to write small, solid and safe control logic for an embedded system, you should generally use C. But if you want to prove it mathematically correct, you'll need to test it with software written in this obscure language from INRIA in Grenoble."

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.

Objective Caml is not the only interesting thing to come out of there.

For a real eye opener, look through the current list of research topics at INRIA. I have (mis)spent hours reading the published papers and source code from some of their projects.

[0] "Equipes de recherche du centre Grenoble" http://www.inria.fr/recherches/equipes-de-recherche/recherch...

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.

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.

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...

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.

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.

According to the people at Ada Core Technologies, that develop gnat, the GNU Ada compiler, all compliance tests has been done using the -O2 flag with the compiler. Thus that mode should be the most tested and reliable option for generating code.

I have no problem believing that aerospace people distrust optimizers. They are in fact unlikely to trust anything before they have inspected the assembler output from the compiler.

It's been my experience that the aerospace industry distrust anything that's less than 30 years old. A lot of people have died from trying to introduce new technology, so they do kind of have a point. However, I think they have mostly learned the wrong lessons from the past.

Wrong is almost always contextual. If the cost of a false positive is that someone dies, and the cost of a false negative is that development is slower, guess which one is chosen?

Slow development also costs lives. One of the major causes of accidents in small plains is simply running out of fuel because the pilot forgot to fill up on the ground and or did not check the fuel gauge in the air. Now, there are a lot of ways to prevent these accidents, but at some point you need to change basic design elements and not just make a longer check list.

> accidents in small plains

Quick development has its drawbacks as well, as you so beautifully demonstrated.

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.

Just trying to avoid a lawsuit.

No, not just trying to avoid a lawsuit, it's actually true. Largely because of garbage collection.

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).

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.

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.

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...

Can your friend prove the Haskell and ML compilers he is using are 100% bug free as well? And the hardware it is running on? (both the compiler and the execution environment if they differ)

If you're interested, the German Verisoft project [1] aims at such pervasive verification. AFAIK they haven't yet verified anything matching the complexity of seL4, but they did verify a simple real-time OS. Of course you do need to stop somewhere, as in trusting something "blindly" (say, the verification tools themselves and the hardware they run on).

[1] http://www.ertos.nicta.com.au/publications/papers/Klein_08.p...

Formal methods != safety-critical.

I think it'd be a hard sell to use ML in safety-critical systems due to the non-deterministic runtime of the GC and potential for memory exhaustion.

As a counter-example, C doesn't prevent formal methods - FWIW VxWorks puts out Arinc 653 and MILS products that are verified* using formal methods.

* - This is carries the following caveat, I believe the core OS is formally verified but the particular BSP/configuration needs be tested/certified by the customer or at the customer's expense.

However, there is a lot of work on generating C code from formal models in Haskell or ML. Verify the high level code; verify the compiler; target a subset of C whose semantics you understand. See e.g. L4; Lustre; Copilot.

IIRC type systems based on linear types are quite promising for making a version of ML without a garbage collector --- there could be some interesting progress here soon!

Being non-deterministic is a non-starter for safety or mission critical systems.

One of the foundational concepts of safety-critical design is strict scheduling of resources. The schedule must be strictly deterministic. The process must get it's work done in the time allocated because the scheduler will move on regardless. It's why you don't do recursion in safety-critical systems. Strictly speaking, you're not even supposed to use while loops in safety-critical systems. In the five years I worked in avionics, the only time I saw a while loop was in code review where the person who wrote it (always a new person) was directed to take it out.

All that being said, safety-critical software production is more about the processes than coding. Even crappy programmers can be taught how to write good safety-critical code when the company adheres to best practices.

As far as the original post, Ada and C. Ada has tremendous support for concurrency and is stable as the day is long. Not much in the way of libraries, but honestly not that important on the kinds of projects you would use Ada to build.

> In the five years I worked in avionics, the only time I saw a while loop was in code review where the person who wrote it (always a new person) was directed to take it out.

I can understand the concern about loop termination, but what is the alternative? Are for loops without a hardcoded upper limit allowed? Or must all loops be unrolled?

The target code for the seL4 project is actually written in C. They do however use Haskell as a stepping stone (they have an abstract spec of their system, which they then prove is implemented by a Haskell implementation, which is in turn implemented by the C implementation).

Do you have any links to your friends work?

> 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.

> 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.

That is the absolute major issue with doing safety-critical development right: it has a cost, that cost is very, very high, and few want to pay it.

One of the few groups I'm aware of which does pay it is the (now defunct, I guess) software shuttle group. Their work was expensive, it was process-heavy (the 1997 story on them quoted 2500 pages of spec for GPS integration which ended up totaling 6.3kloc change to the source, 1.5% of it) but they delivered exactly what they were set to: critically safe code (in fact, if I remember correctly the Shuttle software group is the only area of NASA Feynman praised in his Challenger report)

> That is the absolute major issue with doing safety-critical development right: it has a cost, that cost is very, very high, and few want to pay it.

This is absolutely true. The costs to manage complexity now seem high when software is being built. The costs of managing that complexity in the future are far higher and may have to be paid in lives.

I wonder whether it would be possible to make a lint-like verifier which rejected code whose local complexity exceeded some objective thresholds. I imagine it would be pretty easy to come up with an objective measure of pure control flow complexity, but the complexity of interactions between control and data would be harder to quantify.

Interesting idea. Instead of aiming for something hard and true, you can probably find a good proxy of complexity fairly easily. Once you have it, just don't confuse the map with the territory; but use it as a hint to see what code to investigate.

Global complexity might not be much harder to measure than local complexity, perhaps even easier. Look for interdependencies.

At work I set up one of our project's automated build to fail if the cyclomatic complexity of a method exceeds 20. It's a C#/.NET project so we use NCover as part of the automated build. NCover has a reporting tool that you can set to return a non-zero return value (which will fail most build systems) if it's metrics exceed some value -- in this case class-level cyclomatic complexity exceeding 20.

I've thought about ratcheting it down to 15 based on stuff I've read, but unfortunately that particular failure metric can only be set as low as the class-level in the latest version. The next version (4.0) will have the ability to set the threshold at the method level.

In any case, I'd rather have a handful of places in the code where someone has to do something goofy to work around that metric rather than accidentally allow the whole project's complexity to creep up as time goes on.

> At work I set up one of our project's automated build to fail if the cyclomatic complexity of a method exceeds 20.

Are your co-workers cool with that? Complexity metrics are a little "squishy", but the costs of a broken build are large.

There's the 'pmccabe' tool, which can check for # of lines of functions and their cyclomatic complexity.

Then,

  pmccabe `find . -name '*.c'` | sort -nr | awk '($1 > 10)'

gives me all functions that have a cyclomatic complexity over 10; I often add it as a target in a Makefile, so I can easily check this. Similar, for functions of a certain length.

Tools for measuring code "complexity" already exist. Cyclomatic Complexity is a popular metric:

https://en.wikipedia.org/wiki/Cyclomatic_complexity

checkstyle is a Java lint that, among other things, can check code complexity:

http://checkstyle.sourceforge.net/config_metrics.html

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.

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.

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.

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...

"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...

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.

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.

Making the front page on HN is a sure fire way to get a SO question closed.

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.

This continuously happens on StackOverflow. If a question can be remotely considered to be contentious it will very likely be closed. Quite a few times this has included Qs selected for their newsletter!

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.

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.

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?

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.

I think Haskell's lazy evaluation may make more difficult to verify formally because execution time and memory usage are less predictable.

Use Haskell+Agda to generate a subset of C. You also don't seem to understand what formal verification means. It's a verification of correctness, not resources.

In Real-time systems the two are synonymous. If you run-out of memory or fail to finish a vital calculation in a prescribed amount of time, your program is not correct. See Rate Monotonic Analysis for an example of verification (used in both formal and semi-formal situations) of time.

Where did you get this definition? Formal verification is named as such because it uses "formal methods" (mathematical proofs) to verify the behavior of the program. Your definition isn't formal verification, it's just... verification. You can't formally verify performance any more than you can formally verify physics.

All formal verification requires some assumptions. For example, you might assume that a cosmic ray isn't going to alter a bit in your instructions stream (or you might be developing for outer space and you assume that no more than X bits will be flipped in a given amount of time).

Certain assumptions can make it trivial to verify the performance of code (e.g. assume all memory accesses miss cache and happen right at the beginning of a DRAM refresh for the address you are accessing).

That usually ends up too crappy, so you bound the worst case a bit more by using the cache-replacement model of the CPU you are using. Writeback cache make this analysis quite difficult which is one of many reasons for the existance of writethrough cache. In any event, given a certain execution model, it is tractable to bound the worst-case performance of a system formally.

The UK's national air traffic system used ADA, not haskell.

Let's not forget that Fortran is used in many of the world's Nuclear power plants

MISRA C is a restricted subset of C designed by the Motor Industry Software Reliability Association for use in automotive and embedded systems.

http://www.misra-c.com/Activities/MISRAC/tabid/160/Default.a...

https://en.wikipedia.org/wiki/MISRA_C

I wonder: is safety-critical the same as fault tolerant. Or are those two mostly independent concepts.

I can see safety critical software, software that has been verified to a very high degree to not contain faults. I see fault tolerant software software that does have internal faults but can recover quickly and often transparently to the user.

I find it interesting that there is no mention of using dependently typed languages or proof engines for this application. Something like Coq, where you write the formal proof of correctness as you write the program, would fit the bill nicely if you really care about safety over ease of implementation.

The comment about the cost of formal methods growing "exponentially" with project size is clearly false.

I wouldn't say "clearly" false, though it depends on what you mean by "cost". In a computational complexity sense, most methods are exponential, barring some special-case methods, though in practice you can scale up to pretty big problems anyway. For example, SMT solvers have complexity growing exponentially with the problem size, unless you greatly restrict the formalism, but can verify fairly large designs. The techniques I know of for verifying multithreaded programs have cost growing exponentially with the number of threads as well.

He seems to be talking about proofs by hand, though, where you model a protocol mathematically and then write out a paper proving the protocol to be have desired properties. I have no idea if anyone's tried to quantify how that kind of complexity scales.

I don't know how it scales either, but I'd guess that if your proofs grow even quadraticly with code size then you're doing something wrong. Exponential growth is just clearly wrong. Note that even for SMT solvers, there is not exponential growth with program size. Even with small programs, the model space can be infinite, and general automated theorem proving is undecidable, not NP. Do you have evidence that a million line program is inherently harder to check with an SMT solver than is a thousand line program? Both are probably jut checking approximations to the model.

Similarly, with multi-threading, either the program works for a simple reason that it's author understands, or its correctness is not understood (and it probably doesn't work). People don't work through exponentially increasing number of cases in a growing project, and nor will formal proofs.

Do you have anything to substantiate your claim? I worked on formal methods and state explosion is a very real problem. The state of the program is essentially a subset of a Cartesian product of all variables. Even if all your 'n' variables are binary you still have a state space of potential size of 2^n.

Right, and if your program uses a linked list, the state space is infinite! Correct programs written by humans are correct for reasons that don't require exhaustive case analysis.

Here's some food for thought. Are GC-based and/or lazy-evaluation based languages suitable for safety critical and mission critical apps? It's more difficult to reason the execution time and the memory cost for these functionality.

While C or C++ can be used when coupled together with static analysers, I think I would go with Ada.

SCADE! barring that, Ada and C.

Intricately tied to the choice of the OS.

Reply on news.ycombinator.com