Each of these things can be managed with process. It's not an all-or-nothing strategy. The overall system and application changes in unexpected ways, but as yo

Each of these things can be managed with process. It's not an all-or-nothing strategy. The overall system and application changes in unexpected ways, but as you get lower down the stack, the amount of churn is reduced. Hence, there are strategies to design systems and applications so the most high-assurance pieces are those least subject to change, and that the application code itself runs at the lowest assurance level. Of course, Dijkstra was more of an academic, but this can be managed in real systems with engineering process. A system that is 20% formally verified is safer and has fewer defects than one that is 0% formally verified. The key is applying engineering to this to ensure that the time and budget spent on this specification provides the most benefit.