You're building a strawman. I've never heard of that myth, the saying is more like "if a Haskell program compiles, it usually works". And you can say the same t

You're building a strawman. I've never heard of that myth, the saying is more like "if a Haskell program compiles, it usually works". And you can say the same thing about a couple of other statically typed, functional programming languages. --- > "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that Actually languages can help a lot. This isn't just about "silly mistakes". Compilers are _theorem provers_. Quite literally there's an equivalence between type theory and mathematical logic. I hope you're not saying that math logic doesn't help in modeling real world semantics. So yes, via modelling types in an expressive language you can at least have proof that the changes you make are consistent with the world view you had before those changes. Of course people accustomed to less expressive languages like Java won't believe this until they see it. But you should really look into Haskell to see the difference. And dependent typing brings this to the next level.