Ask HN: Languages for safety-critical embedded work?

[randomacct44]

I'm interested to hear from the HN crowd what's out there in terms of languages / frameworks for doing safety-critical embedded development on commonly-available hardware like the ESP8266. Think at the safety level of implantable medical devices or flight control software.

My usual Google skills aren't getting me anywhere on this one :)

[danielvf]

1. If you are developing for the ESP8266, your current choices are C, Lua, and Arduino. So you are pretty much using C by default.

2. The automotive industry has a standard for safety critical C code. It's called MISRA C. A few of the rules are stupid, but others will save you worlds of issues. You have to buy the PDF from the committee's website for about 15 bucks, but it's worth reading and mostly following.

3. If you are actually writing medical or flight control software, you cannot depend on a single proccesor or computer. Perfect software is not enough. Airliners have three separate computers, each containing three different processor architecture processors, each processor running code compiled on a different compiler, and all checking each others work. SpaceX runs at least five separate embedded linux computers for any critical systems. These communicate in such a way that they can tolerate even malicious actions by any two computers. Google "byzantine fault tolarance"

[RealityVoid]

I fully agree with your analysis of MISRA C.

The issue I have with it is that some people seem to be refusing using their brain when following rules. For exampe, MISRA static checkers compain if you do:

  x = 250

So I've seen people do:

  #define TWO_HUNDRED_FIFTY 250
  x = TWO_HUNDRED_FIFTY

And it drives me insane that people see some rules but don't actually understand what they're for and just skirt around it in the stupidest way possible.

[burfog]

Well, it's a stupid rule. There are times when a plain old number is more maintainable. You don't have to name it, you don't have the extra line of code, you can immediately see what the number is, etc.

[RealityVoid]

I disagree. There are a few cases where a number is more expressive - I even think MISRA has exemptions for 1, 0 and FF.

But in most cases what I want is not the number, it's the _meaning_ of the number. Be it the Command ID, ram block Address or whatever it is. Generally, having code sprinkled with magic numbers is pretty shitty.

In my view:

  a = a<<18;
  a |= b<<8;
  a |= c;

is a kosher use of numbers. But

  case(ChoiceID):
    switch 1:
      /* Do somethin'*/
    break;
    switch 26:
      /* Do somethin' else*/
    break;
    default:
    break;

is not. Generally, numbers are ok as long as you express mathematical ideas nut not ok when you express logical ideas.

[burfog]

Heh, you disagree, then go on to agree. You even provide an example! Another good one is computing the Hamming weight, where the code is far more understandable if you have the numbers right there.

Even your "switch 26" isn't always bad. If the value only occurs in exactly that one place in your code, it's probably better to use a comment in plain English. A comment is more readable than DO_SOMETHIN_ELSE and, normally, would go right in the place where you actually use the value.

[burfog]

Don't overlook the fact that lots of bug-finding tools support plain old C best. Yes yes, it needs them more, but... at least the tools exist!

Get all the tools. There are free tools like "sparse", a tool Linus wrote for his kernel. There are expensive tools like Coverity. Get them all. Use them all.

Build your code with all the warnings enabled. Use multiple compilers, even if they don't compile for your target.

[atomical]

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

[viraptor]

Ada is known for those kind of applications. Very restrictive types / contracts make it a good choice.

Of course a lot of safety critical stuff is still written in C or C++. They may not be perfect, but they're not terrible choices.

[inetsee]

Ada has been used a great deal in the past for military applications, including flight control software for military planes. One of the real advantages of Ada is that there are a number of tools designed to make sure that Ada programs are about as safe as it is possible to make software.

I can't help wondering if some of the problems the F-35 is having is because its software development is being done mostly in C++ and C.

Unfortunately, I would be really surprised if there is an Ada toolchain that can produce code for a microcontroller like the ESP8266.

[viraptor]

GNAT seems to have no problem with that: https://github.com/RREE/esp8266-ada/wiki/Steps-for-building-...

[Tomte]

Depends on the field. Aeronautics and reactor control seem to use "safer languages" like Ada quite a bit.

In factory automation I have only ever seen C, and AFAIK automotive is the same (they seem to be more open to C++, though).

Most of safety-critical development (as I know it -- again, no satelites or nuclear stuff) is documentation, testing and FMEAs. Quite a bit of "patterns" or procedures, as well, like memory testing in the background, redundant variables, cross checks between controllers, plausibility checks etc.

But very, very little focus on saner programming languages.

[eric_bullington]

Ada. I personally lean more and more toward functional languages these days, but despite that, I'm incredibly impressed with modern Ada. Particularly the Spark subset of Ada, which is perhaps the best-thought out, more coherent, most secure language around for general programming. It's the epitome of a well-engineered project, with excellent tooling, and formal verification options to boot. If I had to build something safety critical, I wouldn't hesitate to choose Ada.

And it looks like some folks have already been using Ada on the ESP8266, here are instructions: https://github.com/RREE/esp8266-ada/wiki/Steps-for-building-...

[kognate]

The Power Of 10 is a good place to start.

https://en.wikipedia.org/wiki/The_Power_of_10:_Rules_for_Dev...

The summary would be:

Use vanilla C with some rules about things like memory, testing, and recursion. Testing and static analysis are your friends.

[probinso]

+10 points for Ada. Great language. Barnes book is a great resources

[samfisher83]

I work on industrial control and we typically just use C.

[technion]

This is a tangent, but Wikipedia says this about that chip:

    The ESP8266 is a low-cost Wi-Fi chip with full TCP/IP stack and microcontroller capability produced by Shanghai-based Chinese manufacturer, Espressif.

Am I alone in the concern that in a safety critical environment, the phrase "low cost" should be more of a concern than the choice of language?

[randomacct44]

Totally not :) Just for reference, I'm not actually planning to build a safety-critical device with an ESP8266.

What piqued my curiosity was this project:

http://openaps.org

It's basically a homebrew controller implementation that uses data from a continuous blood glucose monitor to talk to an insulin pump. They're using Node and JavaScript from what I can tell from the GitHub. They're obviously conservative for safety concerns. The code runs on a Raspberry Pi 3.

This got me wondering - what language WOULD be used in 2016 to code something safety-critical? Is there anything coming from research that's better than C? My initial thoughts were something like Elixir, but really anything strongly type-checked and verifiable. Rust was another thought I had.

Looking at this my immediate thought was also "what's the tiniest micro that could do this job instead of the power-hungry Pi?".

I guess everything is C or assembler in the end anyway :) The impression I get from these responses is that a restricted subset of plain C seems to be the most practical solution today.

EDIT: I'm the OP if it isn't obvious, different account.

[technion]

Thanks for the clarification.

I had a look around and I can only guess that the extensive hard limits that they document in their design fulfil the safety requirements on their own.

[superboum]

If you want to go further, you might be interested by proving your software and formal method, something like the B-Method ; https://en.wikipedia.org/wiki/B-Method

Unfortunately, I only know their name and never use it.

[spraak]

Really out of my realm but maybe Rust?

[viraptor]

Probably a nice choice in a few years, but at this point it's rather experimental on anything but main, supported platforms.

[jotux]

Just do what JPL does: http://lars-lab.jpl.nasa.gov/JPL_Coding_Standard_C.pdf