[lmm]

> Give me Java and a real-world problem vs someone using using Scala and I will beat them on the initial write, and destroy them on the maintenance. :)

Seems we have a true disagreement.

> Idris? In the entire history of computing there has been a single[1] complete non-trivial (though still rather small) real-world program (CompCert) written in a dependently typed language.

Five or ten years ago how many such programs were there in a language with higher-kinded types? Thirty years ago how many with type inference? Innovation is slow - perhaps five years was too optimistic, looking at the history - but it does happen; PLT ideas do eventually make their way into mainstream languages.

> although you didn't say it can work, only that it would "be a better language than Scala", so I'm not sure what your success metrics are

I think it will be the most effective (for real-world problems) general-purpose programming language - a spot I think Scala currently holds. Hard to define objectively of course.

[pron]

First, higher-kinded types is a feature; dependent types is an entire philosophy. Second, I think you're misjudging the adoption of those languages/ideas: the percentage of real-world programs using HM type-systems (and similar) has hardly changed in the past two or even three decades. Scala is special because it's a single language with lots of paradigms. If you count only those who make good use of sophisticated typed abstractions in Scala and add those to the HM languages, there would still be a very small uptick. The major change in the past few years, I think, has to do with mainstream adoption of higher-order functions. That idea took fifty years to break into the mainstream.

As to language effectiveness, I can't argue with you because neither of us has any real data, but I can say that there's a lot of religion surrounding the question of how much linguistic features (as opposed to extra-linguistic ones, like GC) actually increase productivity. What is certain is that we still haven't broken the 10x productivity boost Brooks said wouldn't happen between 1986 and 1996, and it's been thirty years -- not ten -- and it seems like we won't do it in another decade.

[lmm]

> higher-kinded types is a feature; dependent types is an entire philosophy

Totality is a philosophy; you can have dependent types as a feature without it. Maybe immutability or purity are better comparisons for what Idris brings to the table, but if you're just talking about dependent types then I'm using them already.

> the percentage of real-world programs using HM type-systems (and similar) has hardly changed in the past two or even three decades.

Is that really true? I can't imagine a recruiter asking about Haskell, or a Facebook-sized company talking about their OCaml strategy, ten years ago.

> As to language effectiveness, I can't argue with you because neither of us has any real data, but I can say that there's a lot of religion surrounding the question of how much linguistic features (as opposed to extra-linguistic ones, like GC) actually increase productivity.

That feels like gerrymandering your definitions to me. GC is usually a language-level feature.

> What is certain is that we still haven't broken the 10x productivity boost Brooks said wouldn't happen between 1986 and 1996, and it's been thirty years -- not ten -- and it seems like we won't do it in another decade.

How would we tell? The productivity of the technology industry as a whole has certainly risen enormously. My general impression is that coding is the bottleneck a lot less often - even for a technology company - than it was five or ten years ago.

[pron]

> Is that really true? I can't imagine a recruiter asking about Haskell, or a Facebook-sized company talking about their OCaml strategy, ten years ago.

I think it may have risen a tiny bit but here's why I think it appears larger than it is: I don't think a recruiter would ask about Haskell today outside a very small section of the ecosystem, but that section seems just larger than it is. What has changed in the past 20 years is the cultural prominence of the startup culture (SV startups hardly make up a minuscule percentage of the software industry, yet they get a significant portion of the media coverage), and even then only if you're involved in communities like Reddit and HN.

I think it is more an artifact of those communities that using certain languages lends a certain prestige, which is then used as a marketing effort (the CTO of a well known SV startup once told me that they have a small team using Scala only so they could attract a certain crowd). Similarly, in Facebook, it is my understanding that Haskell isn't really spreading, but is more of a marketing gimmick to developers of a certain sort in an environment with very unique characteristics. The entire software development industry consists of, I'd make an educated guess, 20 million developers or more (extrapolating from the known number of ~10M Java developers). I would be immensely surprised if more than a million of them can tell you what Haskell is (and by that I mean "a pure functional language").

So there's definitely an uptick in numbers and a rather strong uptick in exposure -- assuming you're following the right online communities -- but I don't think there's a real uptick in portion of production systems. Some people used Lisp and ML in production 20 years ago, too. They just didn't have HN to tell everyone about it. I'm not even sure we're currently at '80s level. Haskell is certainly talked about and used less than Smalltalk in the '80s, and see where it is today.

What is definitely true that some ideas that had previously been associated with functional programming, most notably higher-order functions, have now finally made it into nearly all mainstream languages.

> That feels like gerrymandering your definitions to me. GC is usually a language-level feature.

I think the distinction between language-level abstractions and something like a GC (or dynamic linking) is rather clear, but I won't insist.

> How would we tell? The productivity of the technology industry as a whole has certainly risen enormously. My general impression is that coding is the bottleneck a lot less often - even for a technology company - than it was five or ten years ago.

Is it? I've been a professional developer for 20 years and while I agree that productivity has gone up considerably (maybe 2-3x) it can be attributed nearly entirely to automated tests and GCs.

[lmm]

Ten years ago even startups were largely Java-only when I looked (at least here in London). Five years ago nowhere was advertising pure-Scala/Haskell/OCaml/F# jobs at all. I heard about OCaml at Facebook from friends working there before the big public announcements about it. It's hard to separate general trends from my own trajectory of course.

> Is it? I've been a professional developer for 20 years and while I agree that productivity has gone up considerably (maybe 2-3x) it can be attributed nearly entirely to automated tests and GCs.

I think productivity is noticeably higher than even five years ago, when we already had GC and widespread testing.