3 ms·
> he believed in building a formal specification of software and then proving that the software matched this specification. Given unlimited time and budget, pl
by Hendrikto 3y ago
> he believed in building a formal specification of software and then proving that the software matched this specification.
Given unlimited time and budget, plus the guarantee that things won‘t need to change in unexpected ways, that would be great.
- throwaway290 3y agoThe spec does not have to be infinitely precise and can exist under budget constraints.
- nanolith 3y agoEach 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.