4 ms·

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

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.

pron 11y ago
Because Haskell's design has always placed verification as a top priority. Indeed, Haskell tries (IMO, unsuccessfully so far) to combine programming and verification in a single language. In fact, for some time, Haskell's colloquial tag line was "if it compiles it works" -- what is that if not verification? 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.
- semigroupoid 11y ago
  > "if it compiles it works" I think this wasn't meant literally. I think it rather means that a program that type-checks is at least more likely to work than a dynamically typed one. I think this is far from verification. > 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.
  - pron 11y ago
    > I think this is far from verification. 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).
    - tome 11y ago
      > "helps write more correct code faster due to the rich type-system" -- which is formal verification No it's not. It's an informal probabilistic statement based on induction, not formal reasoning based on deduction. Stop trolling.
      - pron 11y ago
        > not formal reasoning based on deduction Formal verification is not the same as deductive proof. Some formal methods produce "probabilistic statements based on induction".
        tome 11y ago
        You know what? I'd like to ask you a personal question. 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?
        tome 11y ago
        Ah right. It's you who gets to define the word "verification" and Haskell is aiming to do it, yet failing to do it, whether its creators and proponents like it or not. An easy way to both start and win an argument!
        tome 11y ago
        Seeing you edit this post once every five minutes is really quite jarring.
- tome 11y ago
  > Because Haskell's design has always placed verification as a top priority. Indeed, Haskell tries (IMO, unsuccessfully so far) to combine programming and verification in a single language. No it doesn't. Troll.

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.

pron 11y ago

Because Haskell's design has always placed verification as a top priority. Indeed, Haskell tries (IMO, unsuccessfully so far) to combine programming and verification in a single language. In fact, for some time, Haskell's colloquial tag line was "if it compiles it works" -- what is that if not verification? 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.

semigroupoid 11y ago
> "if it compiles it works" I think this wasn't meant literally. I think it rather means that a program that type-checks is at least more likely to work than a dynamically typed one. I think this is far from verification. > 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.
- pron 11y ago
  > I think this is far from verification. 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).
  - tome 11y ago
    > "helps write more correct code faster due to the rich type-system" -- which is formal verification No it's not. It's an informal probabilistic statement based on induction, not formal reasoning based on deduction. Stop trolling.
    - pron 11y ago
      > not formal reasoning based on deduction Formal verification is not the same as deductive proof. Some formal methods produce "probabilistic statements based on induction".
      - tome 11y ago
        You know what? I'd like to ask you a personal question. 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?
      - tome 11y ago
        Ah right. It's you who gets to define the word "verification" and Haskell is aiming to do it, yet failing to do it, whether its creators and proponents like it or not. An easy way to both start and win an argument!
      - tome 11y ago
        Seeing you edit this post once every five minutes is really quite jarring.
tome 11y ago
> Because Haskell's design has always placed verification as a top priority. Indeed, Haskell tries (IMO, unsuccessfully so far) to combine programming and verification in a single language. No it doesn't. Troll.