>if it was really that helpful, more people would be applying it and the benefits would speak for themselves. They've been around a long, long time, though, and never caught on - it's hard not to conclude that there's probably a reason.
My impression is that there are actually not that many business domains where a large investment in time and money to get domain logic correctness from 98% to 99.99% correct is actually called for.
Formal methods are a large investment, too. No two ways around it.
Also, while they havent really caught on in general, some of their ideas have made it into modern type systems.
My issue with the formal methods community is that it always tended to hand wave away the cost/benefit trade offs. It's not that they didnt see those trade offs (they constantly reiterated that they weren't suitable for every problem) - more that they saw it as someone else's problem to solve to decide which problem, when and why.
Im sure if somebody wrote a blog post that provided a sensemaking framework for WHEN formal methods are appropriate vs waste your time it would be popular.
I see hints of this all over the thread - e.g. some people seem to believe it works well for state machines (though I suspect they were nontrivial ones), but as a topic it rarely ever seems to be addressed head on. OP certainly doesnt.
I suspect this trope will reiterate again next year with "formal methods! useful! sometimes!". The community has been like this for decades.
My impression is that there are actually not that many business domains where a large investment in time and money to get domain logic correctness from 98% to 99.99% correct is actually called for.
Formal methods are a large investment, too. No two ways around it.
Also, while they havent really caught on in general, some of their ideas have made it into modern type systems.