3 ms·
> Are you saying there have been studies that show Haskell's type system has not been correlated to higher correctness than say Java or Python, or are you sayin
by pittma 7y ago
> Are you saying there have been studies that show Haskell's type system has not been correlated to higher correctness than say Java or Python, or are you saying you are unaware of any such studies?
On the contrary! Consider for instance: "Total Haskell is Reasonable Coq"[1]
1. https://arxiv.org/abs/1711.09286 https://arxiv.org/abs/1711.09286
- pron 7y agoThis has absolutely no bearing on the matter. The fact that some simple propositional logic statements could be proven using Haskell if Haskell were total, does not mean it has a significant impact on correctness (which requires predicate logic) even if Haskell were total, and it certainly doesn't mean that it's more effective at increasing correctness than Python. And, BTW, Coq is not a particularly effective tool for writing correct software, either. The largest software whose correctness was largely verified in Coq (CompCert) is positively tiny compared to standard software (it's less than 1/5th of jQuery), and the cost was huge. So Coq's "correctness score" of increased correctness per unit of effort is not particularly stellar compared to alternatives.