I've been writing Haskell for 12 years so I'm aware of the abstractions it offers. At the end of the day though, either we're building a bridge or we're not. I

I've been writing Haskell for 12 years so I'm aware of the abstractions it offers. At the end of the day though, either we're building a bridge or we're not. If we're building a bridge (i.e. a distributed database, a real time system, fly by wire system, etc.) Haskell is useless if for no other reason than how it does memory allocation. Dependent types are also a dead end for building bridges in my opinion. Proving any non trivial invariants is basically impossible in the real world (http://web.archive.org/web/20200113205635/http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://web.archive.org/web/20200113205635/http://blog.parall...). And even if it wasn't, dependent types are for a program. But our "bridges" aren't programs, they're systems! If there's one thing that the Haskell community don't understand, it's that. The scary issues that crop up in large scale distributed systems aren't from the nodes, they're from the edges. So any system of correctness that is focused on the nodes [i.e. type systems] is avoiding the real issue. That's the power of TLA+ by the way. By modeling the system, you have a specification that gives you some confidence what you're building is correct before beginning to implement your bridge. And if we're not building a bridge? The business doesn't really care about correctness, they care about shipping features. Rollbacks are an acceptable cost. Our job is to sit down and bang out a solution to the problem at hand, not build the perfect abstraction to the problem. When we use languages like Haskell, we take that power out of product's hands.