Mr Rizzoni, "expert in failure analysis" must have never heard of Ada before. Or, of its use in Airbag steering computers, where the code is mathematically proven to be running correctly.
Isn't that impossible vis-a-vis the halting problem?
For example, designing your program and CPU as a set of state machines allows you to define all possible states of the system (which are deliberately limited), define all the state transitions, then verify that every input condition for each state results in the correct state transition. Even if you simply brute force your way through every state and every transition instead of using mathematical generalizations, you've still proven that the program is correct.
The best research I've seen on this was done with Access Control Matrices in the Computer Security field. e.g. can you prove in a general sense that a sequence of atomic state changes to an ACM result in no violations of access control? The answer is, for atomic state changes you can prove that they are internally consistent, but not that they do not introduce a flaw in the ACM.
In other words, because proving software reduces to proving correctness, it only proves that the software is internally consistent. Basically it's a circular proof. It doesn't prove that the software is without flaw.
But you can write software that can be proven to be correct. You can also write software that can be proven to stay within certain limits (i.e. the computer will fiddle with the acceleration a bit, but not more than a reasonable pre-defined limit, and not when the brake is on).
http://www.google.com/search?client=safari&rls=en&q=...
Years ago, when I looked into it, an "operational" semantics hadn't been defined for Ada, but it seems that the modern language has a defined subset or profile.