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.