> And your comparison of Haskell and Java is particularly interesting. You say that Haskell's type systems is "streets ahead". I agree (although I think this comes at a great cost). However, Haskell correctness or development cost is not "streets ahead" or even noticeably ahead.
I'd argue correctness is in fact streets ahead: orders of magnitude fewer defects (in terms of the code not doing what the programmer intended; the programmer not understanding what some other human intended is still as big a problem as ever) in practice. It's interesting how little value that actually brings in ordinary commercial development, but the correctness techniques will be there when the industry is ready for them. Development cost is much harder to measure; I'd argue that some systems developed with Haskell-like type systems would simply not have been possible to make without them, but that's the sort of question that's very difficult to answer objectively.
> orders of magnitude fewer defects (in terms of the code not doing what the programmer intended; the programmer not understanding what some other human intended is still as big a problem as ever) in practice.
I don't see that, and I'm not aware of any report that reports that.
> It's interesting how little value that actually brings in ordinary commercial development, but the correctness techniques will be there when the industry is ready for them.
Except that in some cases it's already true. Companies like Amazon and Microsoft are seeing great value in using TLA+ and other formal methods, and now management encourages engineers to use them. I just don't see it for Haskell. Facebook is a good example, as they invest a lot in correctness research (both formal methods, like Infer, as well as inductive methods for automatic bug fixing and codegen[1]) and they also use some Haskell. But they're pushing hard on formal and inductive methods, but not so much on Haskell. I don't think correctness is a problem that cannot be addressed, and I believe there are techniques that address it. I just don't see that Haskell is one of them.
> Development cost is much harder to measure; I'd argue that some systems developed with Haskell-like type systems would simply not have been possible to make without them, but that's the sort of question that's very difficult to answer objectively.
I'd argue correctness is in fact streets ahead: orders of magnitude fewer defects (in terms of the code not doing what the programmer intended; the programmer not understanding what some other human intended is still as big a problem as ever) in practice. It's interesting how little value that actually brings in ordinary commercial development, but the correctness techniques will be there when the industry is ready for them. Development cost is much harder to measure; I'd argue that some systems developed with Haskell-like type systems would simply not have been possible to make without them, but that's the sort of question that's very difficult to answer objectively.