Thanks for being generous with my long post. > Sure, but why? I already explained why. Why do you even care about Haskell at all? > Expressing richer specif

Thanks for being generous with my long post. > Sure, but why? I already explained why. Why do you even care about Haskell at all? > Expressing richer specifications in the type systems also has a significant cost. And everything that has a cost should have a benefit or we would abandon the whole enterprise. The simply typed lambda calculus will be 80 years old this year, in June. What was Church going after when he published it to the Journal of Symbolic logic? If you go back and read it he was trying to make sense of the lambda calculus. That calculus gave us one branch of computing as we know it but it was not sufficiently expressive enough to make logical statements about different classes of functions: not all functions that have the same shape have the same meaning. In a similar fashion not all programs are created equal. Given a set of functional requirements by a person we can probably independently write programs that satisfy them. Type theory is simply a means for us to reason about these programs. Whether you write your program that enables you to verify the internal correctness of your programs with respect to the type system used to check it or not doesn't matter one bit to the user of the system. To the programmer however, it can matter a great deal. Of the programs we could write in languages that don't allow us to verify the correctness of our programs with respect to a particular type theory all we can say is: when I evaluated the program with these inputs at this time, it worked. We can be reasonably certain it will continue to work and it will likely work on more inputs. Of the programs we write in a language that does allow us to verify the program is logically consistent and sound with respect to a particular type theory is that it is consistent. We would still be obligated to prove that the program meets the specified requirements. But we don't have to worry about whether we forgot to handle a branch, access data that isn't there, over write data we didn't intend to... and a whole slew of things that do plague us in languages without such tools. We can instead focus our effort on proving that we meet the requirements which is a much smaller and more tractable problem. As an engineer I don't see the reason why theory and research must be separate. I see my work as sitting between both worlds: theory informs application which in turn gives me more problems to inform the direction to go. > I just don't particularly like it, for the same reasons some people don't particularly like Python or Java. That's fair, I don't particularly like Java either. But I don't go into threads about Java and ask Java developers why they bother with it. Some of the challenges posted by Stephan are legitimately interesting challenges for Haskell programmers. A dependently typed Haskell would, ironically, make Haskell a more simple language and allow us to continue pushing type-driven programming further for many of the benefits I've described. Many of the benefits to these issues have been described in the article. > it shows virtually no growth after 25 years I beg to differ. Even after 10 years it has shown a lot of growth. TFA opens with celebrating the advances made in the last decade. The reason why Haskell isn't as popular as many mainstream languages, if it's so great, is network effects. Javascript is as popular as it is because it was the only language available for a long, long time on a platform many people wanted to write software for. Ruby would not even be on the radar if it wasn't for it's killer app: Rails. I dabbled in Ruby before Rails came along -- it was super obscure -- but no matter how good it was without Rails it would have languished in obscurity, I think. Some languages became popular by sheer force: Java was a solution in search of a problem and Oracle had a war chest to make sure people thought about it. I recall a time with Python was incredibly rare and obscure and had similar network effects to over-come. Haskell doesn't have a company or group of companies pumping millions of dollars into its development, is not a platform exclusive, and so far hasn't had a killer application where it excelled over other incumbents (except perhaps in compilers). It also doesn't help that many programmers continue to persist FUD about Haskell for reasons I don't understand. Similar to how people feel justified for being contemptuous of Javascript or PHP I suppose. However if Haskell was the platform-exclusive language of the web for several decades I think this conversation would be completely different. Haskell is a fine language and the reasons for working on effect systems are good ones and I'm excited to see the results. If you don't get why then try harder to understand the work or find something constructive to say about it. The people working on it are brilliant and have good, practical reasons for it.