Sorry, but I don't really get why you are comparing Haskell and the model checkers you listed. Haskell is a programming language and is not meant to be a formal verification tool.
There are more popular languages that are faster than Haskell, languages with better tooling, and languages that are easier to learn and faster to write and read code. Haskell's claim to fame and the justification for its learning curve is verification (both formal and informal). Therefore, I think it's reasonable to compare it with verification tools.
> Haskell's claim to fame and the justification for its learning curve is verification (both formal and informal).
I think Haskell's claim to fame is being a pure language (and maybe its laziness). I don't know what languages you had in mind, but Haskell's learning curve is usually also related to people not being familiar with functional programming as a paradigm.
How would you characterize verification, then? (and remember, most verification methods aren't proofs)
> I think Haskell's claim to fame is being a pure language
Sure, but why would you want to use a pure language? I mean, you could say that any programming paradigm is intellectually interesting, but some people seem to think that using Haskell actually has some real advantages. What are those advantages? Performance? Readability? Sure, some believe it results in more maintainable code, but I think that the most common praises are "helps to reason about code equationally" -- which is informal verification -- or "helps write more correct code faster due to the rich type-system" -- which is formal verification (BTW, I say "believe" and "claim" because unfortunately we don't yet have any significant evidence to speak with confidence regarding Haskell's benefits in large, challenging real-world software because it has hardly been used in any yet).
> Haskell's learning curve is usually also related to people not being familiar with functional programming as a paradigm.
Partly, but I was quite familiar with FP (Scheme, ML) when I started learning Haskell, and there's a very steep curve (steeper than going from Java to OCaml).
No it's not. It's an informal probabilistic statement based on induction, not formal reasoning based on deduction. Stop trolling.
Formal verification is not the same as deductive proof. Some formal methods produce "probabilistic statements based on induction".
What is it that motivates you, at the same time as introducing interesting and pertinent details to a discussion, to be so negative and condescending about other people's choice of technologies?
You are clearly very intelligent and well educated. Why do you feel the need to do this? I can't for the life of me understand where this is coming from. Do you not realise how aggravating it is for the other parties in the discussion?
You have plenty to contribute by mentioning interesting technologies like TLA+ and your threading implementation. Why do you have to dump on other people at the same time?
An easy way to both start and win an argument!
No it doesn't. Troll.