Why Don't People Use Formal Methods? – 2019

I love the promise of formal methods. I've been coding professionally since 1992 and to this day, I don't have a better way to get started on a software development task than "give me the gist of what you want, I'll program something, and then we'll tweak it later". Don't get me wrong - I've spent cumulative years of my life sitting through week-long design sessions where the loudest, most opinionated people in the room argue back and forth about trivial, inconsequential details and produce 600+ page documents that no human could possibly read, but none of them have ever had any bearing on the finished product. So I like the idea of having a definite process to go through - however complex - that will result in indisputably superior software.

However, even if I were to spend - what, a month? - learning TLA+, I doubt I'm persuasive enough to actually force its adoption in any organization, and there's no real evidence that companies that are actually successful are using it either.

All my latest projects do have a `make verify` target. It's not much work, and it tests much more than 100% code coverage. I'm always surprised what kind of weird bugs it finds. Eg in my CTL (the STL in C) it found the 3way comparison problem, which was just recently added to the STL.

Perhaps a lack of compelling success stories? There are lots of approaches that work well on paper but fall apart out in the wild.