> And if you need absolute correctness (when human life depends on the software) you would probably use Ada and Spark or something else that enables you to actually prove correctness.
That's not even absolutely correct, because provability depends on correct preconditions, and there is a universe of incorrect preconditions that can throw a wrench into your provable system.
Your completely 'proven' system fails, when there's a short in jump resistor J35 on the motherboard, which invalidates the entire underpinning of the software system you assume to have.
For critical systems, you should strive for resiliency and failovers, not provability.
In Spark2014, you could at least prove the absence of runtime errors, and in the near future, prove memory safety. Without specifying them since they're part of the semantics of the language. That's not bad for a start.
That's not even absolutely correct, because provability depends on correct preconditions, and there is a universe of incorrect preconditions that can throw a wrench into your provable system.
Your completely 'proven' system fails, when there's a short in jump resistor J35 on the motherboard, which invalidates the entire underpinning of the software system you assume to have.
For critical systems, you should strive for resiliency and failovers, not provability.