The extreme end of this is dependent types, which is so strong that it can be used as a foundation for mathematics itself, and is the principle that the Lean, the proof assistance, is used on. A Lean "program" is effectively proven to be bug-free.
Also, just think about this: what bugs have you had in your software historically? How many of those do you believe would've been prevented by a type system like Haskell's?? At least for my software, nearly every bug is a logical bug that no type system could've prevented (though I do use typed languages like Java and Kotlin).
The only thing that ever made a difference in the number of bugs in any study I've seen was not the language, but good testing and the experience of the developer.
> A Lean "program" is effectively proven to be bug-free.
You misunderstand this. Lean proves the program matches a specification. It doesn't and can't prove the specification is for the "right thing" - in other words, if your specification itself has wrong or bad assumptions, you'll still have bugs. Now, who is going to prove the specification is specifying the "right things"? It's turtles all the way.
> You're not going to get any "credible empirical evidence" already because the sample size is so small. That would require getting, say, 100 companies that are similar in size and tasks, have a working business model and are still around, and also want to spend time on methotically collecting concrete evidence, and care to blog about that.
> people don't really want to spend time stating the obvious
> We don't spend time blogging that on our Haskell server, we get pretty much none of [run time type error or segfault] because well, those don't exist in Haskell
> We're convinced it's the best tool for the server job, compared to other tech we used at past jobs and projects. So we're using Haskell for it, and we started it in Haskell. We cannot compare before/after, because we directly started it in the "best tool available". We can compare our current project to our past individual work experience, but one cannot simply turn such individual cross-project experience into quantitative evidence
https://www.reddit.com/r/haskell/comments/1plsmqh/comment/nt...
> Also, just think about this: what bugs have you had in your software historically? How many of those do you believe would've been prevented by a type system like Haskell's??
I program Haskell all the time, and I encounter "non-bugs" where the compiler prevented me from doing something, which other languages would not have, on the regular.
> (though I do use typed languages like Java and Kotlin)
Those are not even close to a Hindley-Milner based type system like the one in Haskell.