Well, yes. But that's the feature in this context. The point is: places where Ada is used require certain levels of qualification and certification, all the way

Well, yes. But that's the feature in this context. The point is: places where Ada is used require certain levels of qualification and certification, all the way down to the compiler. You have to be able to prove that that binary fragment was produced by that particular code fragment. Think aircraft, nuclear reactors, rockets. So this tooling is already certified and it fills the "compiler + various verification tools" space. Otherwise you'd have to certify your tool chain yourself every time it changes. Say you are building an aircraft. The whole software stack is part of the aircraft certification, all the way down to the compiler. A complete aircraft is a system composed of other systems which themselves are composed of other systems. Eventually, there's a software system. Systems are certified independently and for a complete configuration. Of course, requirements get stricter as the criticality of the component increases. Not every component has such strict requirements as discussed above. But a lot of them do.