11 ms·

What's The Best Language For Safety Critical Software?

109 points by pooriaazimi 14y ago

kaolinite 14y ago
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.
- pooriaazimi 14y ago
  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/ http://ertos.nicta.com.au/research/l4.verified/ [2]: http://www.linuxfordevices.com/c/a/News/NICTA-sel4-OK-Labs-OKL4/ http://www.linuxfordevices.com/c/a/News/NICTA-sel4-OK-Labs-O...
  - thalur 14y ago
    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)
    - oggy 14y ago
      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.pdf http://www.ertos.nicta.com.au/publications/papers/Klein_08.p...
  - jbester 14y ago
    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.
    - dons 14y ago
      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.
    - njs12345 14y ago
      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!
    - Czarnian 14y ago
      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.
  - oggy 14y ago
    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?
- jvanenk 14y ago
  > 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.
  - masklinn 14y ago
    > 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)
    - jvanenk 14y ago
      > 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.
  - 14y ago
- tseabrooks 14y ago
  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.
protomyth 14y ago
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 14y ago
  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.
  - alephnil 14y ago
    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.
  - Retric 14y ago
    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.
    - stcredzero 14y ago
      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?
      - Retric 14y ago
        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.
jonnycowboy 14y ago
SCADE! barring that, Ada and C.
shasta 14y ago
The comment about the cost of formal methods growing "exponentially" with project size is clearly false.
- deleted 14y ago
  [deleted]
- _delirium 14y ago
  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.
  - shasta 14y ago
    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.
- mynegation 14y ago
  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.
deleted 14y ago
[deleted]
masklinn 14y ago
> 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 14y ago
  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.
kitsune_ 14y ago
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 14y ago
  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/ 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.
pooriaazimi 14y ago
(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 14y ago
  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 https://news.ycombinator.com/leaders ).
  - ent 14y ago
    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.
    - pooriaazimi 14y ago
      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?
rmcclellan 14y ago
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.
SteveJS 14y ago
Making the front page on HN is a sure fire way to get a SO question closed.
- jsdalton 14y ago
  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.
  - amouat 14y ago
    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!
_djo_ 14y ago
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.
- ajross 14y ago
  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.
  - alexchamberlain 14y ago
    Literally?
    - ajross 14y ago
      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.
      - 14y ago
tuxguy 14y ago
Intricately tied to the choice of the OS.
vbtemp 14y ago
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.
josefonseca 14y ago
"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-40th-anniversary-one.html http://googlecode.blogspot.com.br/2009/07/apollo-11-missions...
- vbtemp 14y ago
  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 14y ago
  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.
deleted 14y ago
[deleted]
gregholmberg 14y ago
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/ http://caml.inria.fr/ [1] "Success Stories" http://caml.inria.fr/about/successes.en.html http://caml.inria.fr/about/successes.en.html [2] "OCaml: a serious contender" http://caml.inria.fr/about/programming-contest.en.html http://caml.inria.fr/about/programming-contest.en.html edit: clarity
- tjr 14y ago
  What language was the primary control software written in?
  - gregholmberg 14y ago
    " ... a subset of the C programming language".
    - tjr 14y ago
      Er, I missed that footnote. Thanks.
      - gregholmberg 14y ago
        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."
        deleted 14y ago
        [deleted]
- pgroves 14y ago
  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.
jpro 14y ago
Let's not forget that Fortran is used in many of the world's Nuclear power plants
kamaal 14y ago
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 14y ago
  Just trying to avoid a lawsuit.
  - javert 14y ago
    No, not just trying to avoid a lawsuit, it's actually true. Largely because of garbage collection.
oggy 14y ago
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.pdf http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFS-ccs10.pd...
digler99 14y ago
Is Ada code in aerospace really "safe" for the muslim civilians that got bombs dropped on their head ? I think a language that's applied toward blowing people up is kind of dangerous, actually.
spitfire 14y ago
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 14y ago
  I think Haskell's lazy evaluation may make more difficult to verify formally because execution time and memory usage are less predictable.
  - Locke1689 14y ago
    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.
    - aidenn0 14y ago
      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.
      - Locke1689 14y ago
        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.
        14y ago
Arcticus 14y ago
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.
npsimons 14y ago
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-Stavely/dp/0201385953 http://www.amazon.com/Toward-Defect-Programming-Allan-Stavel...
gm 14y ago
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 14y ago
  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.
nobby-w 14y ago
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?
Nelson69 14y ago
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 14y ago
  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.
ww520 14y ago
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.
Craiggybear 14y ago
Ada and Eiffel are still very much in the frame. I don't know Eiffel but Ada certainly used to have a very fine reputation for military applications among other things.
pjmlp 14y ago
While C or C++ can be used when coupled together with static analysers, I think I would go with Ada.
cpeterso 14y ago
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.aspx http://www.misra-c.com/Activities/MISRAC/tabid/160/Default.a... https://en.wikipedia.org/wiki/MISRA_C https://en.wikipedia.org/wiki/MISRA_C
rdtsc 14y ago
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.
zwadia 14y ago
Missed JOVIAL: http://en.wikipedia.org/wiki/JOVIAL http://en.wikipedia.org/wiki/JOVIAL Pretty important uses in the Air Force.

109 points by pooriaazimi 14y ago

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.

pooriaazimi 14y ago
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/ http://ertos.nicta.com.au/research/l4.verified/ [2]: http://www.linuxfordevices.com/c/a/News/NICTA-sel4-OK-Labs-OKL4/ http://www.linuxfordevices.com/c/a/News/NICTA-sel4-OK-Labs-O...
- thalur 14y ago
  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)
  - oggy 14y ago
    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.pdf http://www.ertos.nicta.com.au/publications/papers/Klein_08.p...
- jbester 14y ago
  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.
  - dons 14y ago
    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.
  - njs12345 14y ago
    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!
  - Czarnian 14y ago
    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.
- oggy 14y ago
  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?
jvanenk 14y ago
> 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.
- masklinn 14y ago
  > 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)
  - jvanenk 14y ago
    > 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.
- 14y ago
tseabrooks 14y ago
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.

protomyth 14y ago

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 14y ago
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.
- alephnil 14y ago
  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.
- Retric 14y ago
  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.
  - stcredzero 14y ago
    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?
    - Retric 14y ago
      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.

jonnycowboy 14y ago

SCADE! barring that, Ada and C.

shasta 14y ago

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

deleted 14y ago
[deleted]
_delirium 14y ago
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.
- shasta 14y ago
  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.
mynegation 14y ago
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.

deleted 14y ago

[deleted]

masklinn 14y ago

> 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 14y ago
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.

kitsune_ 14y ago

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 14y ago
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/ 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.

pooriaazimi 14y ago

(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 14y ago
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 https://news.ycombinator.com/leaders ).
- ent 14y ago
  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.
  - pooriaazimi 14y ago
    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?

rmcclellan 14y ago

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.

SteveJS 14y ago

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

jsdalton 14y ago
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.
- amouat 14y ago
  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!

_djo_ 14y ago

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.

ajross 14y ago
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.
- alexchamberlain 14y ago
  Literally?
  - ajross 14y ago
    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.
    - 14y ago

tuxguy 14y ago

Intricately tied to the choice of the OS.

vbtemp 14y ago

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.

josefonseca 14y ago

"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-40th-anniversary-one.html http://googlecode.blogspot.com.br/2009/07/apollo-11-missions...

vbtemp 14y ago
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 14y ago
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.

deleted 14y ago

[deleted]

gregholmberg 14y ago

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/ http://caml.inria.fr/ [1] "Success Stories" http://caml.inria.fr/about/successes.en.html http://caml.inria.fr/about/successes.en.html [2] "OCaml: a serious contender" http://caml.inria.fr/about/programming-contest.en.html http://caml.inria.fr/about/programming-contest.en.html edit: clarity

tjr 14y ago
What language was the primary control software written in?
- gregholmberg 14y ago
  " ... a subset of the C programming language".
  - tjr 14y ago
    Er, I missed that footnote. Thanks.
    - gregholmberg 14y ago
      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."
      - deleted 14y ago
        [deleted]
pgroves 14y ago
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.

jpro 14y ago

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

kamaal 14y ago

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 14y ago
Just trying to avoid a lawsuit.
- javert 14y ago
  No, not just trying to avoid a lawsuit, it's actually true. Largely because of garbage collection.

oggy 14y ago

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.pdf http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFS-ccs10.pd...

digler99 14y ago

Is Ada code in aerospace really "safe" for the muslim civilians that got bombs dropped on their head ? I think a language that's applied toward blowing people up is kind of dangerous, actually.

spitfire 14y ago

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 14y ago
I think Haskell's lazy evaluation may make more difficult to verify formally because execution time and memory usage are less predictable.
- Locke1689 14y ago
  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.
  - aidenn0 14y ago
    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.
    - Locke1689 14y ago
      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.
      - 14y ago

Arcticus 14y ago

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.

npsimons 14y ago

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-Stavely/dp/0201385953 http://www.amazon.com/Toward-Defect-Programming-Allan-Stavel...

gm 14y ago

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 14y ago
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.

nobby-w 14y ago

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?

Nelson69 14y ago

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 14y ago
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.

ww520 14y ago

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.

Craiggybear 14y ago

Ada and Eiffel are still very much in the frame. I don't know Eiffel but Ada certainly used to have a very fine reputation for military applications among other things.

pjmlp 14y ago

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

cpeterso 14y ago

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.aspx http://www.misra-c.com/Activities/MISRAC/tabid/160/Default.a... https://en.wikipedia.org/wiki/MISRA_C https://en.wikipedia.org/wiki/MISRA_C

rdtsc 14y ago

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.

zwadia 14y ago

Missed JOVIAL: http://en.wikipedia.org/wiki/JOVIAL http://en.wikipedia.org/wiki/JOVIAL Pretty important uses in the Air Force.