> Get back to me when the formal methods actually generate high quality code that cannot deviate from the spec That would be useful but there is a fundamental

> Get back to me when the formal methods actually generate high quality code that cannot deviate from the spec That would be useful but there is a fundamental issue: code is too specific. İn formal specification you usually don't specify that detailed but you specify the general behaviour of the system. So usually the specification corresponds to a lot of programs with subtle differences. That's why code a documentation falls short: you don't know what is intentional and what is just a random choice. It's simply too specific to describe high level requirements. The other way around (verification of program with respect to the specification) can be more feasible to implement.