> and also in advancing the state-of-the-art in the software industry, which is another worthy goal, but a very different one. The state of the art doesn't adv

> and also in advancing the state-of-the-art in the software industry, which is another worthy goal, but a very different one. The state of the art doesn't advance until practitioners share the results of adopting new techniques and tools. How else would the SWEBOK guide [0] have a section on unit testing if, in study, we don't have results that correlate the practice of TDD with a reduction in software errors, productivity, or some form of correctness? Is it irrational of us to practice TDD anyway? How do we know formal methods are effective if there hasn't been a large scale study? An interesting example of this balance between research and practice came to me from learning about the construction of cathedrals, particularly the funicular system of Guadi [1]. Instead of conventional drawings he used hanging models of the structures. It was not widely practiced or a proven method but it enabled him to reduce his models to 1:10th the scale and accurately model the forces in complex curves. As he shared his work and others studied it the state of the art advanced. > .. or at all. > I think Haskell is OK -- not much better or much worse than most languages, but not my cup of tea -- and Lean is very interesting for those interested in formal logic, but offers little to engineers I think we're at, or approaching, the point where we're talking past each other. I heard the talk from the Semantic team at Github on their experience report with algebraic effects sounded positive [2]. They are probably the largest production deployment of a code base exploiting algebraic effects. Their primary area of focus is in semantic analysis of ASTs. And yet they would like to continue pushing the state of the art with algebraic effects because, in their words, In Haskell, control flow is not dictated by the language, but by the data structures used. Algebraic effect interpreters enable them to interpret and analyze unsafe code without having to maintain buggy, difficult to reason about exception-based work flows. They say this singular feature alone is essential for rapid development. Yes, they're doing research. However their research isn't in answering hypothesis about effect interpreters. It's directly contributing to an interesting feature in one of the largest code-sharing platforms in the world. They were able to exploit algebraic effects so they could focus on their research, their real-world problem, without having to fuss around with the limitations of conventional mainstream languages. I do wish more companies using Haskell would share their experiences with it. It would go a long way to dispelling the pervasive view that Haskell is only good for research. It's not: it's a practical, production ready language, run time, and ecosystem that can help anyone interested in using it to tackle hard problems. In a similar fashion I think dependent types would make working with types in Haskell easier. Instead of having to learn the different mix of language extensions you need to enable in order to work with inductive type families, it could be more like Lean, where it's a normal data declaration. Haskell introduces a lot of extra concepts at the type level because it has two different languages. I can simplify a lot of code in libraries I've written if Haskell had dependent types (and I'm working on libraries in Lean that may eventually prove it). It may take a while but I think Haskell will eventually get there. The community has been discussing and researching it for years. It's going at the pace it is because the Haskell community is not focused on pure research: there are a lot of production applications and libraries out there and they don't want to break compatibility for the sake of answering interesting research questions. Despite your opinions on type theory there's a real, practical reason I might exploit Rank-2 types or Generalized Algebraic Data Types and it's not simply to answer a pressing hypothetical question: I've used these in anger. I hope some of this answers your questions as to why get there at all? [0] https://www.computer.org/education/bodies-of-knowledge/software-engineering https://www.computer.org/education/bodies-of-knowledge/softw... [1] https://en.wikipedia.org/wiki/Church_of_Col%C3%B2nia_G%C3%BCell https://en.wikipedia.org/wiki/Church_of_Col%C3%B2nia_G%C3%BC... [2] https://github.com/github/semantic/blob/master/docs/why-haskell.md https://github.com/github/semantic/blob/master/docs/why-hask...