This dismisses theorem proving as too difficult to use for existing systems. My experience with old, complex systems is that they’re often old, complex and not

This dismisses theorem proving as too difficult to use for existing systems. My experience with old, complex systems is that they’re often old, complex and not very well understood anymore. Theorem proving is all about producing a specification and asking software to help you certify its correctness. I get that it’s often very hard in practice, but wouldn’t this process be incredibly beneficial then for existing systems? The endeavor would likely motivate the creation of an up-to-date spec and prove or disprove its correctness all at the same time. Whether the existing implementation matches the spec is another challenge, but this could at least uncover serious design flaws in high assurance software.