Someone else posted a danluu study that is very good. I've read many more studies over the years and NEVER seen one showing a significant advantage for Haskell and similar languages. Try Google Scholar and you'll find some for sure.
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.
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.