I've long been intrigued by pure FP, advanced type systems and proof assistants from an academic point of view but haven't yet been convinced that the effort in

I've long been intrigued by pure FP, advanced type systems and proof assistants from an academic point of view but haven't yet been convinced that the effort involved in learning such systems/methods pays off in most cases (without taking into consideration the costs you still have when you already know the methods well). I will still try to learn more about this, but without any strong conviction that this needs to be immediately useful. By contrast, I've only more recently started hearing more and more about model checkers such as TLA+. The case studies in this blog post serve to give a good motivation for why such systems might be useful (as well as honestly presenting drawbacks; something that advocates of e.g. PFP rarely do). I would love to use something like that one day. As an aside, I still think it's a disgrace how irrelevant empirical research is to most aspects of today's software development. Another blog post by the author cites a paper claiming that very simple testing, especially of error conditions, would be able to prevent a huge chunk of production bugs, but things like that are rarely talked about. The whole profession is unfortunately amateurish and always obsessed with fads and trends instead of taking a more analytic and empirical approach which makes me sad.