Interesting food for thought! I like your dual approach of "better process" and "better language".
What are the safer languages out there?
I like to think Safe-D (a safer subset of the D programming language) is safer. But it is not ultra-safe in the complete and comprehensive static analysis sense that SPARK 2014 can claim.
There are different ways to think about safety. Languages that have automatic bounds checking for example are safer than those without (Java vs C).
Another aspect is whether the language can be proven formally. SPARK is one example and I believe I read that several of the functional languages (or subsets of them) are formally provable.
I read an article that said that Airbus is experimenting with model-driven development for critical systems because making sure that even Ada was correct was too difficult and costly. So, they just want to build a model and have software convert it into correct source code. Obviously that's a very specialized use case that's unlikely to gain widespread use in the near future.
Here's a link to AdaCore's product that might be similar to what Airbus is doing (code generation tools are over my head): adacore.com/qgen
We're a place where coders share, stay up-to-date and grow their careers.
We strive for transparency and don't collect excess data.