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.
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)
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.
Global complexity might not be much harder to measure than local complexity, perhaps even easier. Look for interdependencies.
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.
Are your co-workers cool with that? Complexity metrics are a little "squishy", but the costs of a broken build are large.
Then,
pmccabe `find . -name '*.c'` | sort -nr | awk '($1 > 10)'
https://en.wikipedia.org/wiki/Cyclomatic_complexity
checkstyle is a Java lint that, among other things, can check code complexity:
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...
[1] http://www.ertos.nicta.com.au/publications/papers/Klein_08.p...
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.
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.
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?
Do you have any links to your friends work?