alt Hacker NewsI think every formal methods phd student who's interested in adoption of their techniques/tools has a short bout of doubt/depression upon realizing just how large of a surface area for bugs lives in a sufficiently useful specification.
This is deeply related to the conceptual error a lot of executives are currently making around automation in/of their software engineering orgs.
It has always been true that learning some formal methods probably makes you a better programmer in certain ways, even if you never use them. I think it's increasingly also true that learning some formal methods probably makes you a better manager of people/processes that product software.
Execs will often hand-wave away complexity as being irrelevant detail. And sometimes it is - especially if an urgent directional decision is needed.
The key skill - which is rare - is knowing exactly how much analysis to do.
Formal methods are appealing because they suggest that full analysis is possible. But formally proved programs can still have bugs!