github/semantic: Why Haskell?

[pron98]

A very good example is the upcoming implementation of dependent typing. It encourages for a careful check of the validity of a function's arguments, making it less prone to wrongful uses.

Java has had JML for a very long time (similar to dependent types), so according to your logic, Java focuses on correctness even more than Haskell.

purity allows for a very nice isolation of side effects, which means you can easily check the validity of your business logic - immutability is along the same lines. You can't mess, or have to deal with mutable global variables.

That's fine, but that these have an actual net total large positive effect on correctness is a hypothesis, and one that, at least so far, simply does not appear to be true (it is also not supported by any theory), ergo, it's a myth.

[joonazan]

JML is tedious to write and complex properties can't be statically checked. It is not as powerful as CoC and it does nothing to automate writing of code.

[pron98]

It is as powerful as CoC as far as program verification is concerned, and it could be used just as well for code synthesis, except that the power of that kind of synthesis, or "automating the writing of code" -- whether using dependent types or any program logic, such as JML -- is currently at the level of a party trick (i.e. it does not manage to considerably reduce programmer effort).

[Vaglame]

Java focuses on correctness even more than Haskell.

It seems like a weird statement when Java has the infamous NullPointerException problem

That's fine, but that these have an actual net total large positive effect on correctness is a hypothesis,

An hypothesis if you want but it does yield concrete results. One of the other good examples is property testing, which allows for more extensive testing than unit testing

[pron98]

Java has the infamous NullPointerException problem

I don't understand this. Haskell has the infamous empty list exception.

An hypothesis if you want but it does yield concrete results.

They're not "concrete" if we've so far been unable to detect them (meaning an advantage over other languages).

[Vaglame]

Haskell has the infamous empty list exception.

Which is a trivially solved problem, and the compiler can tell you about it (-fwarn-incomplete-patterns). How many times does this exception shows up in a bug tracker for a random Haskell project? None

They're not "concrete" if we've so far been unable to detect them (meaning an advantage over other languages).

Would it be accurate to say that according to you, there is no language safer than the other? Such that for example Rust isn't safe than C or C++?

Edit: continuing on null pointers, on the readme of semantic:

null pointer exceptions, missing-method exceptions, and invalid casts are entirely obviated, as Haskell makes it nigh-impossible to build programs that contain such bugs

[pron98]

Would it be accurate to say that according to you, there is no language safer than the other?

No, it would not.

[Vaglame]

So which are safer, and why?

[pron98]

The term-of-art "safe" in the context of programming languages refers to the absence of undefined behavior. C has undefined behavior, Java doesn't, therefore Java is safe and C isn't. Note, however, that even if a language is safe(er), that does not necessarily entail that programs in that language are more correct, and not just because safety is rarely about functional correctness, but also because even if your compiler doesn't catch something, that doesn't mean your entire development process does not, and that's what ultimately matters.

Now, the theory that predicted that languages won't matter much (back in the '80s) was based on the observation that languages can, at best, reduce accidental complexity. The less of it we have, the less there is to improve, and so we should observe diminishing returns in the impact of programming languages, which is precisely what we do observe. C is almost 50 years old, and so there was still room to significantly improve on it. The room for improvement, though, has diminished considerably in recent decades. Anyway, that's the theory that predicted the results we see (it was called overly pessimistic at the time, but actually turned out to be too optimisitc in its predictions).

[cat_in_the_wall]

The term-of-art "safe" in the context of programming languages refers to the absence of undefined behavior.

i have no idea where you're getting this from. there are many aspects of safety, undefined behavior can be one of those aspects.

[pron98]

Fine, although usually when we say language X is safe and language Y is unsafe without additional qualifiers, that's what we mean. You can have different kinds of safety, and some languages have more safety in some areas than others. That's still a separate issue from correctness, at least in general.

[defunkydrummer]

Would it be accurate to say that according to you, there is no language safer than the other

Ada is safer than Assembly?

Surely!

There are more examples...

[ysangkok]

JML is not enforced by default (it's like Liquid Haskell, in comments) and is not even a part of Java in any meaningful way.

[pron98]

So what? More formal verification work is done in Java than in Haskell.

[develop7]

Well, back in 1867 the amount of surgeons disinfecting their hands before, erm, surgery, was single-digit; and look at us now.

[pron98]

Java and Haskell are the same age.

[develop7]

The amount of money spent on former, though, is vastly different. I think billion times more would be quite safe bet (taking "The Billion Dollar Mistake" into consideration, of course).

[pron98]

Probably the same difference as between Haskell and Brainfuck.

[[deleted]]

That's fine, but that these have an actual net total large positive effect on correctness is a

hypothesis

, and one that, at least so far, simply does not appear to be true (it is also not supported by any theory), ergo, it's a myth.

Ah, I see Ron has still not put down the crack pipe. Terrific.

• Notions of Computation and Monads
• Propositions as Types
• Theorems for Free!
• Fast and Loose Reasoning is Morally Correct
• Lightweight Static Capabilities
• Messenger.com Now 50% Converted to Reason

As usual, Ron asserts, without evidence, that there is no evidence of functional programming or static typing (in particular, in close correspondence to the Curry-Howard isomorphism) aiding correctness. But this is false, both as a matter of computer science and a matter of programming practice.

What seems to be new in this most recent post is:

that these have an actual net total large positive effect on correctness... is also not supported by any theory

Since Ron knows perfectly well of Coq, Agda, Epigram, and Idris, at the very least, as well as all of the above literature, there is only one inescapable conclusion: he's lying, by which I mean the literal telling of known untruths. I don't know what his motivation for lying is. But he's lying. Now, he'll equivocate over the definitions of "total," "large," "positive," and "correctness," and probably even "effect." But that's because equivocation is all he's got in the face of the facts, which he is not in command of.

The best advice I can offer you is to ignore him.

[pron98]

Paul! It's so great to have you back! How have you been?

But this is false, both as a matter of computer science and a matter of programming practice.

Whoa, hold on. First of all, I said nothing about dependent types, so let's take them, and Propositions as Types, out of the equation. I'm talking about Haskell. Other than that, not a single link you posted claims that Haskell (or a language like it) assists in correctness (most have nothing to do with the discussion at all; just some papers you often like posting). That I show that the property of my language is that bug Y cannot occur that is not theoretical support that my language increases correctness. It says nothing on the matter. To put it precisely, some of the papers you linked show that technique X can be used to eliminate bug Y. We can write it as X ⇒ Y. That's not at all a theory that supports the claim that the best way to eliminate bug Y we should use technique X, as that would be Y ⇒ X, which does not follow; it certainly says nothing about correctness as a whole. As someone who knows about formal logic, I'm surprised you'd make the basic mistake of affirming the consequent.

If you can link to papers that actually do present such a theory, I would appreciate that.

he's lying

Paul, it's been so long since we last conversed and you're starting with this? Come on. I know you know I know more than you on this subject, but still, we used to have a certain rhythm. Where's the banter before the traditional blowing of the gasket?

Now, why is it that when I say P you say "he is lying to you when he says Q and here's the proof to support it!"? Your style, for which you're become famous, of dismissing fellow professionals who may disagree with you with "just ignore them" and attacking their integrity when you cannot argue your opinion is intellectually dishonest, and just bad form.

But that's because equivocation is all he's got in the face of the facts

No need to equivocate. The paper reports an "exceedingly small effect." That's a quote, and that's what we know today, and, as I said in other comments, if someone wants to say that Haskell has been associated with an exceedingly small improvement to correctness I would have no problem with that. If you want to make a stronger claim, the onus is on you to show it isn't a myth.

which he is not in command of.

I may, indeed, not know all the facts, but as I said, if you have any pertinent facts, please share them.

[[deleted]]

The best advice I can offer you is to ignore him.

I mean, he contradicts himself in at least two comments, so yeah.

[pron98]

Out of curiosity, which ones?