I think most development occurs on problems that can't be formally modeled anyway. Most developers work on things like, "can you add this feature to the e-comm

I think most development occurs on problems that can't be formally modeled anyway. Most developers work on things like, "can you add this feature to the e-commerce site? And can the pop-up be blue?" which isn't really model-able. But that's not to say that formal methods are useless! We can still prove some interesting aspects of programs -- for example, that every lock that gets acquired later gets released. I think tools like Infer[0] could become common in the coming years. [0]: https://fbinfer.com/ https://fbinfer.com/