6 ms·

You said: "I would like to challenge that by pointing out that not a single piece of large software ... has ever been written using the skills/concepts of the

by willtim 10y ago

You said: "I would like to challenge that by pointing out that not a single piece of large software ... has ever been written using the skills/concepts of the higher levels of this chart." To which I gave two counterexamples (today and on other occasions). All software systems should be modular to some degree, so I am not clear exactly what your criteria for a large software system is. In both my examples, the Haskell codebases are monolithic repositories where everything is typed-checked and built together. You keep asking for quantitative data for a comparison with other languages. But my answer is the same as last week. It's good people that make software efficiently and cheaply. Give engineers PHP and they'll still manage to build something good. Haskell is just a tool, but it's a tool that increasingly good people are asking to use. The system at Barclays and Standard Chartered were built and are currently maintained very cheaply because good people were hired. Haskell just happened to be their preferred tool.

pron 10y ago
> I am not clear exactly what your criteria for a large software system is. Let a "software system" mean any assembly of processes that communicate to provide some shared functionality, with the components being coupled to one another in some non-trivial way (i.e., there are correctness conditions that cross processes boundaries, so that changes to one program may necessitate changes in others). Excluding the compiler, how many lines of Haskell code do you have in your largest system (using my definition)?
- willtim 10y ago
  You just described the entire bank! I prefer my single codebase/single build definition. I forget the current figure, but StanChart has at least 3M lines of (dense) Haskell. More details here: https://skillsmatter.com/skillscasts/9098-haskell-in-the-large-the-day-to-day-practice-of-using-haskell-to-write-large-systems https://skillsmatter.com/skillscasts/9098-haskell-in-the-lar...
  - pron 10y ago
    > I forget the current figure, but StanChart has at least 3M lines of (dense) Haskell Oh, thank god, finally we get a number. It turns out that I was completely wrong, and that in its 20 years of hyped existence, someone has built something big with Haskell once. You may think I'm sneering, but only a little bit, because while one is almost nothing, it is much better than actually nothing because at least it is a first anecdote. Now, who do I have pester to get some more metrics? > More details here: Sadly, there are no more relevant details in that talk.
    - willtim 10y ago
      Just out of interest, are you skeptical of static type systems in general? Because AFAIK there has never been a quantitative study proving their effectiveness, only empirical studies.
      - sheepmullet 10y ago
        There is a lot of evidence that "primitive" static type systems add value via enabling better tooling. Low cost of adoption + clear minor tooling benefits is usually enough evidence to adopt Java/C# style static types. Haskell style static typing has a very high cost of adoption and so must conclusively show a strong benefit in order to be adopted by industry. At the moment I feel Haskell companies can get away with using Haskell because PL enthusiasts are willing to absorb the training costs.
      - pron 10y ago
        I am not skeptical of type systems in general and TBH I've never worked on a large piece of software written in an untyped language (I often program in Clojure, but so far never a large system -- and yeah, I am skeptical about Clojure too even though I love it). But you're mistaken if you think I'm looking for quantitative studies; that's far too high a bar. I am looking for well-researched anecdotes, and there are plenty of them for type systems in general. I am, however, very skeptical of the interpretation some people, especially in typed FP, give to types and the reasons they believe types provide a benefit. For example, the relationship between useful type systems and software correctness is not direct. I am currently using a formal verification tool that is completely logic based (and it has an interactive theorem prover, a model checker, and is backed by decades of careful mathematical analysis of its soundness) which is completely untyped, and yet it is as powerful as Coq for proving correctness of algorithms. If direct, formal, proofs of correctness is what you're after, types might not be the best solution. Types, however, have other clear benefits that are not related to formal correctness, or, at least, not correctness of global program properties.

by willtim 10y ago

pron 10y ago

> I am not clear exactly what your criteria for a large software system is. Let a "software system" mean any assembly of processes that communicate to provide some shared functionality, with the components being coupled to one another in some non-trivial way (i.e., there are correctness conditions that cross processes boundaries, so that changes to one program may necessitate changes in others). Excluding the compiler, how many lines of Haskell code do you have in your largest system (using my definition)?

willtim 10y ago
You just described the entire bank! I prefer my single codebase/single build definition. I forget the current figure, but StanChart has at least 3M lines of (dense) Haskell. More details here: https://skillsmatter.com/skillscasts/9098-haskell-in-the-large-the-day-to-day-practice-of-using-haskell-to-write-large-systems https://skillsmatter.com/skillscasts/9098-haskell-in-the-lar...
- pron 10y ago
  > I forget the current figure, but StanChart has at least 3M lines of (dense) Haskell Oh, thank god, finally we get a number. It turns out that I was completely wrong, and that in its 20 years of hyped existence, someone has built something big with Haskell once. You may think I'm sneering, but only a little bit, because while one is almost nothing, it is much better than actually nothing because at least it is a first anecdote. Now, who do I have pester to get some more metrics? > More details here: Sadly, there are no more relevant details in that talk.
  - willtim 10y ago
    Just out of interest, are you skeptical of static type systems in general? Because AFAIK there has never been a quantitative study proving their effectiveness, only empirical studies.
    - sheepmullet 10y ago
      There is a lot of evidence that "primitive" static type systems add value via enabling better tooling. Low cost of adoption + clear minor tooling benefits is usually enough evidence to adopt Java/C# style static types. Haskell style static typing has a very high cost of adoption and so must conclusively show a strong benefit in order to be adopted by industry. At the moment I feel Haskell companies can get away with using Haskell because PL enthusiasts are willing to absorb the training costs.
    - pron 10y ago
      I am not skeptical of type systems in general and TBH I've never worked on a large piece of software written in an untyped language (I often program in Clojure, but so far never a large system -- and yeah, I am skeptical about Clojure too even though I love it). But you're mistaken if you think I'm looking for quantitative studies; that's far too high a bar. I am looking for well-researched anecdotes, and there are plenty of them for type systems in general. I am, however, very skeptical of the interpretation some people, especially in typed FP, give to types and the reasons they believe types provide a benefit. For example, the relationship between useful type systems and software correctness is not direct. I am currently using a formal verification tool that is completely logic based (and it has an interactive theorem prover, a model checker, and is backed by decades of careful mathematical analysis of its soundness) which is completely untyped, and yet it is as powerful as Coq for proving correctness of algorithms. If direct, formal, proofs of correctness is what you're after, types might not be the best solution. Types, however, have other clear benefits that are not related to formal correctness, or, at least, not correctness of global program properties.