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.<p>My usual Google skills aren't getting me anywhere on this one :)
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.<p>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.<p>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"
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!<p>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.<p>Build your code with all the warnings enabled. Use multiple compilers, even if they don't compile for your target.
Ada is known for those kind of applications. Very restrictive types / contracts make it a good choice.<p>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.
Depends on the field. Aeronautics and reactor control seem to use "safer languages" like Ada quite a bit.<p>In factory automation I have only ever seen C, and AFAIK automotive is the same (they seem to be more open to C++, though).<p>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.<p>But very, very little focus on saner programming languages.
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.<p>And it looks like some folks have already been using Ada on the ESP8266, here are instructions: <a href="https://github.com/RREE/esp8266-ada/wiki/Steps-for-building-on-Linux" rel="nofollow">https://github.com/RREE/esp8266-ada/wiki/Steps-for-building-...</a>
The Power Of 10 is a good place to start.<p><a href="https://en.wikipedia.org/wiki/The_Power_of_10:_Rules_for_Developing_Safety-Critical_Code" rel="nofollow">https://en.wikipedia.org/wiki/The_Power_of_10:_Rules_for_Dev...</a><p>The summary would be:<p>Use vanilla C with some rules about things like memory, testing, and recursion. Testing and static analysis are your friends.
This is a tangent, but Wikipedia says this about that chip:<p><pre><code> The ESP8266 is a low-cost Wi-Fi chip with full TCP/IP stack and microcontroller capability produced by Shanghai-based Chinese manufacturer, Espressif.
</code></pre>
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?
If you want to go further, you might be interested by proving your software and formal method, something like the B-Method ; <a href="https://en.wikipedia.org/wiki/B-Method" rel="nofollow">https://en.wikipedia.org/wiki/B-Method</a><p>Unfortunately, I only know their name and never use it.
Just do what JPL does: <a href="http://lars-lab.jpl.nasa.gov/JPL_Coding_Standard_C.pdf" rel="nofollow">http://lars-lab.jpl.nasa.gov/JPL_Coding_Standard_C.pdf</a>