Hacker News Reader

Comment by tome | Hacker News Reader

I'm going to make a few comment and nitpicks.

"Patronising those outside the faith ... Please drop the condescending tone."

This is a great sentiment, but rather jarring to have it followed up by "No sane person can argue that we want to bifurcate a programming language into distinct base-level and type-level fragments".

"Equivocating around “type-safety”"

Surely it's reasonable to use the terminology "type safety" to describe a range of properties that code may have beyond the (supposed) original meaning of "memory safety".

"If everyone would just use a modern language with a fancy type system, all our correctness problems would be over, right? ... Type systems cannot be a one-stop solution for specification and verification."

This is an enormous straw man. No fan of strongly typed languages claims that they solve all correctness problems. Furthermore, the fans of strongly typed programming are the most likely to appreciate the additional forms of verification that Stephen outlines.

View on HN

> This is an enormous straw man. No fan of strongly typed languages claims that they solve all correctness problems.

I have read the claim "If it compiles, it works" (or minor wording variations), on this board, more than once (in reference to Haskell). Fans of strongly typed languages do in fact make claims that sure sound like they are saying that.

It's said semi-tongue-in-cheek. The original statement was filled with caveats. [0]

Sometimes it's said less tongue-in-cheek. Then it usually has to do with the facts that large refactorings can be handled by merely breaking things and rewiring until types check. This generally does work since types typically guard "wirings".

But taken out of contexts and as the meaning is extended bit by bit it becomes truly ridiculous and nobody would disagree.

So, don't just propagate the rumor. Nobody is claiming miracles. It just sounds like that at around the 8th iteration of the telephone game.

[0]: As far as I'm aware, this is the origin of the idea: http://r6.ca/blog/20120708T122219Z.html

Wow, that link is really something. I never would have thought that someone would release code into the wild without ever running it.

Donald Knuth, IIRC, once said, "Be cautious running the following code; I have only proven it correct, not tested it."

"Beware of bugs in the above code. I have only proved it correct, not tried it."

http://www-cs-faculty.stanford.edu/~uno/faq.html

The origin is definitely further back. I recall hearing "it takes longer to get it compiling, but when it compiles it works" about OCaml more than a decade ago. When I mentioned this to my father at that point, he remarked that the sentiment goes back further.

It goes back to discussions on Ada as well. I, personally, qualify my advocacy with a probably. As in, "if it compiles, it's probably correct."

I wouldn't be terribly surprised if he'd been thinking of Ada evangelists, though I think there are other candidates too. Unfortunately, I can't ask him to clarify...

You know, that's certainly correct. I feel like roconnor's post comes to mind for me because of it's audacity more than its primality. I'll make a note in my original comment if I can.

(Edit: I can't.)

From your link:

"...I actually had no idea how the function worked. I simply wrote a function that matched the required type."

I guess everybody have done that. But releasing it without testing... I'm just impressed, in both a good and a bad way.

Huh, you know, that sounds just like how dimensional analysis affects people sometimes. I've certainly seen some take a pile of engineering inputs and whack them together until the units work (myself included); it's a shockingly powerful heuristic for linear systems, since you'll typically only be off by some logical scaling factor. Of course, there's a bajillion ways it can deceive, so it's wise to be thorough.

It seems entirely reasonable to me to view dimensional analysis as a type system itself.

It has to do with how abstract and parametric the code was. There may very well be only one valid type-checking program which exists (so long as you do a cursory check against infinite loops and error throwing).

So, it's a gamble---do there exist any other non-trivial programs at this type?

If not, then I know my code written is correct without testing.

If there are, then I'm risking that I found the right one.

This is why Haskellers get so excited about "parametricity". It's the core tool that exacts this property of "there are only a small number of programs which could ever exist at this type" which drives correctness.

People get excited when they find out they can have types that are expressive, eliminate many useless bad programs almost for free, and be working in a language more expressive than most.

I don't think "people get excited when they encounter convenient sets of features" is a reasonable excuse for misleading claims like "if it compiles it works."

It is a reasonable explanation for why some people make these claims (over excitement), but they still shouldn't be misleading people like that.

Here I point you to what tome & tel said.

If it's so clearly nuts, why are you picking that interpretation? Do you read everyone's words in the least-charitable/sensible light possible?

I can't speak for lelandbatey. For myself, though, I picked that interpretation because that really seemed to be what they were trying to say. I'm not looking to take peoples' words in the least-charitable way possible, but I'm also not going to go out of my way to make excuses for them when they say something that is clearly wrong.

I cannot say that getting upset over people using jokey memes to communicate ideas (Haskell is more likely to be correct after a successful type-check than other langs) is likely to do you much good.

I like Epictetus for when I notice I am upset about something that isn't within my control: http://classics.mit.edu/Epictetus/epicench.html

So let's see here: You asked why I was picking the interpretation I did. I answered. You respond about me getting upset, and commend Epictetus.

Where, exactly, did I say that I was getting upset? I was stating why I interpreted those guys as being serious rather than joking in their claims. What does Epictetus have to say to whether they were tongue-in-cheek or not? Are you just arguing to argue? Because you're sure not responding to what I said.

> Haskell is more likely to be correct after a successful type-check than (most) other langs

True.

> Haskell is more likely to be correct after a successful type-check than other langs

Is there any empirical evidence for this?

You really don't want to lean on empiricism for PL, but: http://www.cs.yale.edu/publications/techreports/tr1049.pdf

> You really don't want to lean on empiricism for PL

Why not? considering "more likely to be correct" is an empirical claim.

> http://www.cs.yale.edu/publications/techreports/tr1049.pdf

Haskell vs Ada, C++, etc. in 1994.

Because all comparative PL studies are nonsense, including that one.

Look at the experiment methodology described in most of them.

We have something better for evaluating PLs.

> We have something better for evaluating PLs.

Do tell! How do you evaluate empirical claims (about programming languages) without empirical evidence?

Empirical evaluations break down quickly as the complexity of what is being measured increases, so your best bet in doing a study is to focus on one or a few features.

PLs are of course evaluated over time in the market place over time, like any other designed artifact.

I love that report and find it very inspiring (and it gives me an intuition that Haskell has an edge over the other languages), but the methodology is very disappointing:

- The requirements were mostly up to the interpretation of implementors, which more or less decided the scope of their programs.

- All results were self-reported. Even ruling out dishonesty, there are a lot of ways uncontrolled experimenters can report incorrect results.

- Many implementations weren't even runnable.

- No code was run by the reviewers, at all.

I really would love to see a more serious attempt at this experiment (probably with more modern languages).

In this I prefer logical reasoning to empirical evidence. Consider a function that takes a list of things and returns the last one. Let's write that function in Haskell.

last :: [a] -> a

Without looking at an implementation, let's think of how many ways this function could possibly go wrong? It could return the first element of the list instead of the last one. It could return the second to last element of the list. More generally, it could return any one of the elements of the list that was passed in. But that's it (other than the empty list case which for simplicity we can ignore because it's a condition we can statically detect). There are no other possibilities, period.

Now think about implementing this function in any other language. What about Java?

public Object last(Object objs[])

This function can return any of the elements of the incoming array. It could also return null. It could also return the int 42, or the string "hello". It could delete files on your hard drive, open a network connection and phone home to the NSA. I could go on and on.

The point here is that you simply can't say as much about what this function could be doing as we could say about the Haskell version. This is the case for every mainstream language in wide use today. Some languages allow you to say a little more than others, but none of them come close to what Haskell gives you. Because of this, I don't really feel a pressing need for empirical evidence. Logical reasoning lets me make that claim quite confidently.

> There are no other possibilities, period.

That's true! You have proved the original (deductive) claim "if it compiles, it works" for that one specific example, but that does not hold in general.

In general you may prefer the alternative (inductive) claim "more likely to be correct", but that claim requires empirical evidence.

The inductive claim "more likely to be correct" is strongly supported by the evidence gained from enumerating the number of ways the functions could go wrong. Now if we want to expand our domain out from just that function to programs in general, we need an idea of how applicable those ideas are to larger programs. The biggest source of reducing error cases in my example was purity.

Some parts of programs (namely the side effecting parts) can't be expressed as pure functions. So the next piece of evidence we need is an estimate of the percentage of large programs that can be expressed as pure functions. From my experience writing Haskell full-time for the last five years I can tell you that it is very substantial. Even in very impure code you can often factor out lots of small pure operations. I feel very safe in claiming that at least a third of Haskell code can be written with pure functions, and I think it's likely greater than half. (It could be a lot higher, but I'm trying to keep the confidence level fairly high.) You don't have to take my word for this. You can go off and browse through millions of lines of Haskell on [Hackage](http://hackage.haskell.org/packages/) and see for yourself. It probably wouldn't be too difficult to write an automated script to do this.

Now we've seen that pure functions have a small fraction of the error conditions that impure functions have. And we've seen that maybe half of all the code we write can be expressed that way. That's a pretty dramatic reduction in the number of potential error conditions we might encounter for even complex programs. That is why I think the claim "more likely to be correct" is strongly supported by evidence.

> It could be a lot higher

I'd believe 95% LOC don't perform IO, just like any codebase in any language, though it may be easier in Haskell to identify which LOC those are.

But it doesn't matter! The problem could be in the non-IO functions. Take this "scary!" line of code:

    rm -rf "$STEAMROOT/"*

That's a correct IO function (rm -rf) using the result of an incorrect non-IO function ("$STEAMROOT/"*).

I see that as a null error. Using maybe or optional would have solved that problem.

> Using maybe or optional would have solved that problem.

If the code were written correctly then it would be correct!

It's more like "if the code were written like Haskell programmers write programs, taking full advantage of static types to encode information about function return values, then it would be correct. Forgetting to handle the 'null' option would be detected at compile time."

> if the code were written like Haskell programmers write programs [...] then it would be correct

and if the code were written like (true) bash programmers write programs, taking full advantage of "set -u" and "test", then it would be correct.

There is a big difference: "set -u" won't reject incorrect bash programs, it will merely stop some kinds of incorrect behaviors by stopping the program and preventing it from causing greater harm. However, the program won't have completed its intended task, therefore remaining incorrect.

In contrast, using Maybe to indicate "possibly no value" in Haskell (as it is standard practice; in fact there are no nulls in the language) prevents you from even writing some kinds of incorrect programs in the first place. In this sense, a program written in Haskell is a lot more likely to be correct than one written in bash, because the compiler will force you to consider cases you may have missed in a less safe language (like bash).

Of course, neither language guarantees correctness. It's just that one is safer than the other by design.

> "set -u" won't reject incorrect bash programs

No, but "set -u" does help the bash programmer to reject incorrect bash programs and to put "test" where necessary, just as the Haskell compiler helps the Haskell programmer.

Perhaps the Haskell compiler helps more. Perhaps Haskell programs are more likely to be correct. Perhaps. There is only one way to find out.

> It's just that one is safer than the other by design.

What do you mean by this? Is this a deductive claim, contradicting the previous sentence, or an inductive claim that Haskell programs are "more likely to be correct" (all else being equal), which requires empirical evidence, as you cannot establish an inductive claim with deductive arguments.

> "set -u" does help the bash programmer to reject incorrect bash programs and to put "test" where necessary, just as the Haskell compiler helps the Haskell programmer.

Except the Haskell compiler (GHC here) doesn't just equivalently put test "where necessary", but it puts test everywhere and on everything which would be wildly impractical and tedious with bash.

@infraruby

> No, but "set -u" does help the bash programmer to reject incorrect bash programs and to put "test" where necessary, just as the Haskell compiler helps the Haskell programmer.

> Perhaps the Haskell compiler helps more. Perhaps Haskell programs are more likely to be correct. Perhaps. There is only one way to find out.

I think you're being disingenuous. Haskell is designed to be safer (i.e. able to reject more incorrect programs) than bash. There is no "perhaps" here -- I've shown how the compiler helps more. In your example, bash simply fails to reject an incorrect program. The program will NOT run as intended, but instead will abort when it reaches an inconsistent state (such as attempting to access an uninstantiated variable). Do you see the difference between finding out at run-time that your program misbehaves, as opposed to entirely preventing the misbehavior at compile time? You simply cannot write a Haskell program that will attempt to reference an undeclared variable. That's a whole failure mode entirely gone! You don't even need to test for this, because Haskell is comparatively safer than bash.

> I've shown how the compiler helps more.

If the Haskell programmer uses Maybe, but there is also a cost to doing that, and overall that approach may (or may not) help more in writing correct programs than using bash with a test suite using "set -u".

> The rest of your comment reads like a confused mess to me.

You have two options: 1. you can make deductive claims like "if it compiles then it works" which require proof; or 2. you can make inductive claims like "more likely to be correct (all else being equal)" which require empirical evidence.

You appear to be offering deductive arguments for an inductive claim.

> If the Haskell programmer uses Maybe, but there is also a cost to doing that

No, no ifs about it. Haskell uses Maybe to denote the absence of a value; this is a fact. There is no other possibility because the language doesn't have null values. If there to a cost in using Maybe, it's definitely not paid in safety/correctness, which is what we're discussing here.

You continue to write "may or may not" but I've shown you how the approach is better than bash. You can even forget the Maybe monad if you're less experienced with it, and instead focus on one simple fact: you can write and run a bash program that aborts after attempting to access an undeclared variable, but you cannot write and run such a program in Haskell because it's impossible. Haskell is safer.

Deductive/inductive is neither here nor there. I didn't make the ridiculous claim that "if it compiles then it works", and nobody else here did either. The claim I did make is that entire failure modes which are present in bash aren't possible in Haskell; I leave to you as an exercise to consider whether there exist failure modes in Haskell which are not in bash.

> Haskell uses Maybe to denote the absence of a value

A Haskell programmer could use an empty string for that, or given a Maybe could do this:

    fromMaybe ""

But no true Haskell programmer would do that.

> you can write and run a bash program that aborts after attempting to access an undeclared variable

Yes, and perhaps the bash programmer could likely eliminate that fault through testing, perhaps about as likely as the Haskell programmer could get the Haskell compiler to accept a program at all!

> The claim I did make is that entire failure modes which are present in bash aren't possible in Haskell

And therefore Haskell programmers are more likely to write correct programs?

> A Haskell programmer could use an empty string for that, or given a Maybe could do this: fromMaybe ""

Do you see how that's totally unrelated to accidentally accessing an uninitialized variable? In one case, you have an unforeseen event, usually caused by a typo; because the programmer didn't plan for this, the program will abort, crash or launch nuclear missiles, depending on the non-statically typed language of your choice. In the other case, the programmer who chooses to use fromMaybe has to decide what the actual default is, and since he has to consciously pick one, he will choose a useful one. Also, because he is using Haskell, if he wants to express "there is no meaningful value", he will always use Nothing. Feel free to reply to this with yet another snark, but it will only show you're unfamiliar with the subject under discussion.

> perhaps the bash programmer could likely eliminate that fault through testing, perhaps about as likely as the Haskell programmer could get the Haskell compiler to accept a program at all!

No. While testing may eliminate some of these errors, it's even better if they cannot happen at all. That way you can focus your time on testing actual errors. A language which automatically disallows some classes of errors is safer than one where you have to remember to check for them. Note: safer, not necessarily better. I'm not saying Haskell is "better" than Ruby, if that's why you're being so defensive about this: there are valid reasons why one would choose a language which offers fewer guarantees of correctness (i.e. there are "safer" languages than Haskell, and valid reasons not to pick them as well).

> > The claim I did make is that entire failure modes which are present in bash aren't possible in Haskell

> And therefore Haskell programmers are more likely to write correct programs?

Yes, fewer failure modes -> increased probability of correctness.

My advice to you: stop being sarcastic, because it's not helping your argument. Also, how many Haskell programs have you written, or at least code reviewed, since you're so sarcastic about how a "true" Haskell programmer writes code?

> Do you see how that's totally unrelated to accidentally accessing an uninitialized variable?

I was responding to your comments about Maybe, but, yes, that is a separate issue.

> While testing may eliminate some of these errors, it's even better if they cannot happen at all. That way you can focus your time on testing actual errors. A language which automatically disallows some classes of errors is safer than one where you have to remember to check for them.

Perhaps. But perhaps it makes no actual difference in practice. And perhaps the cost of using Haskell, of satisfying the compiler, of fixing type errors that would not be (runtime) errors in a dynamically-typed language, perhaps that cost outweighs any benefit that type-checking may provide.

I don't know. And neither do you.

This entire thread I have asked for empirical evidence, but you have offered only deductive arguments, and that's fine, do as you like, but it's not persuasive.

> Yes, fewer failure modes -> increased probability of correctness.

That's an interesting hypothesis.

I wonder what would be found in a comparative study of statically-typed Haskell code developed with the help of the compiler vs dynamically-typed Haskell code (more failure modes!) developed with the help of an interpreter (if this is possible). Using the same core language would eliminate many confounding variables.

BTW, have you not heard "no true scotsman" before?

> perhaps the cost of using Haskell, of satisfying the compiler, of fixing type errors that would not be (runtime) errors in a dynamically-typed language, perhaps that cost outweighs any benefit that type-checking may provide.

That's completely irrelevant to the current discussion. We are not discussing convenience; we're discussing safety. Are you trying to de-rail the debate? :)

By the way, because you're intent on "teaching" me what deduction and induction mean: not that it has anything to do with the argument at hand, but deductive reasoning (when you can apply it) trumps inductive.

> > Yes, fewer failure modes -> increased probability of correctness.

> That's an interesting hypothesis.

That's... uh... that's not an hypothesis. Something that can fail in fewer ways is safer than something that can fail in more varied ways, all else being equal. There is no need for inductive reasoning here.

> BTW, have you not heard "no true scotsman" before?

I have, and I have also noticed you were trying to sarcastically invoke this fallacy all along. Unfortunately, it seems you've misunderstood it: No True Scotman applies when you make an assertion, then you're presented with a contradiction, and in order to counter it you adopt an ad hoc assertion which serves as an exception. The fallacy doesn't apply when the assertion is not ad hoc, but in fact that which defines the original assertion. Haskell programmers program using Maybe, that's not a "No True Scotman" fallacy. For example, if I said "Haskell programmers do X", and you say "that's not true for Haskell programmers using Ruby!" and I counter "I was talking about Haskell programmers using Haskell", that's not a case of No True Scotman. It's the same for Haskell programmers using the Maybe monad.

Let me explain the kind of flawed reasoning you've been using so far. Say you read something about handguns with safeties being safer than handguns without safeties. You start "blah blah inductive reasoning no true scotman yadda yadda". When someone counters, "well, are you saying handguns with safeties designed to make them safer are not actually safer than handguns without safeties?" your reply seems to be "well, if you give the handgun with safety to a kid, load the gun, switch the safety off, and tell the kid to pull the trigger, then it's not safer!".

Do you see the ridiculousness of your position? Any Turing complete language can be used improperly and cause harm. But some languages are safer than others by design. Not better, merely safer. For example, Haskell is safer than Ruby :)

> We are not discussing convenience; we're discussing safety.

We were discussing whether Haskell programs are more likely to be correct (than bash programs), all else (including convenience) being equal. Who is more likely to write correct programs, for the same effort: a Haskell programmer or a bash programmer? Did you think we should allow the Haskell programmer more time, to satisfy an inconvenient type-checker?

> you make an assertion, then you're presented with a contradiction, and in order to counter it you adopt an ad hoc assertion which serves as an exception.

That is exactly what you did!

You said "Haskell uses Maybe", I said "A Haskell programmer could [do something else]" and then anticipated a no true Haskell programmer fallacy, but you went right ahead anyway: the programmer who chooses to use fromMaybe has to decide what the actual default is, and since he has to consciously pick one, he will choose a useful one. Also, because he is using Haskell, if he wants to express "there is no meaningful value", he will always use Nothing.

But let's make it official: if Angus writes fromMaybe "", which is accepted by the Haskell compiler but deletes all my files, is he a Haskell programmer?

> Say you read something about handguns with safeties being safer than handguns without safeties.

Is that an empirical study, or just a salesman saying "it has a safety therefore it's safer!"

A safety may provide less safety than other measures, for the same effort. Obviously, using a safety is not much effort. How much effort is required to satisfy the Haskell compiler? And how does that compare to other measures? That is an empirical question.

A safety may provide no safety for people who always handle firearms safely. Perhaps bash programmers who always follow conventions (just as true Haskell programmers always follow conventions) in practice would never deploy programs that access uninitialized variables (for example). Where can I find these bash programmers? That is an empirical question.

A safety may reduce safety in situations where a firearm must be used quickly. How quickly can a Haskell programmer fix a critical bug when the Haskell compiler reports type errors that would not be runtime errors in a dynamically-typed language? That is an empirical question.

A safety may induce risk-compensation. Perhaps Haskell programmers often throw caution to the wind, believing that Haskell programs are more likely to be correct anyway, no empirical evidence needed! How many Haskell programmers believe that? That is an empirical question, but obviously there are quite a few :-p

> But some languages are safer than others by design.

What do you mean by "safer" here? Let's say "type-safety" means "a type-checker enforces some constraints" and "practical-safety" means "more likely to be correct, all else being equal". It seems you think "type-safety" == "safety" == "practical-safety", by definition.

> Haskell is safer than Ruby

By how much? How much more, exactly, are Haskell programs likely to be correct?

Your post can be pretty much answered with a big "no".

- No, we were talking about safety, not convenience. Stop shifting the subject. (But do you know what IS inconvenient? Being hit by a bug on production in your Ruby program that could have been prevented by a static type checker).

- No, this is not a case of No True Scotsman. First, you seem to misunderstand how fromMaybe is used (have you EVER programmed in Haskell?). Unlike other languages, where null can hit you by surprise, the programmer ALWAYS chooses the default value for fromMaybe. Since HE chooses it, it's not an accident. It can never happen by accident, as with null. Repeat after me: this. is. not. a. case. of. the. no. true. scotsman. fallacy. "So there is this Scottish guy..." "Wait, what if this is a Scotsman from Mars?" "But Scotsmen are from Scotland!" "A-HA! Fallacy!" This gets old fast.

- No, a programming language with additional safeties is logically safer than one without, all else being equal (i.e. if no other safeties get removed instead). Especially since those safeties don't prevent you from also applying every engineering practice from the other, no-safe language. You can do all the fancy testing you do for your Ruby programs in Haskell as well! In fact, a lot of interesting testing tools have come from the Haskell community, such as QuickCheck (aka property testing). In fact, it wouldn't surprise me if there was a RubyCheck nowadays.

- No, Haskell programmers aren't smug fools who believe that because their programs compile then they must be correct, and therefore no additional testing or QA is necessary. You keep bringing this old nonsense up, and you're the only one who believes it. Please accept as a given that no-one believes this and never bring it up again.

> What do you mean by "safer" here? Let's say "type-safety" means "a type-checker enforces some constraints" and "practical-safety" means "more likely to be correct, all else being equal". It seems you think "type-safety" == "safety" == "practical-safety", by definition.

Actually, rather than being equal, what I think is that an increase in one implies an increase in the other. A type-checker enforcing some constraints automatically makes your language practically safer than one without it. It's yet another tool in your toolset, one that gets automatically applied by the compiler. I get that, by convenience, some people want to write programs without some safeties; that's an issue of convenience, which is separate.

> Obviously, using a safety is not much effort. How much effort is required to satisfy the Haskell compiler?

Not much. Haskell programmers everywhere do it daily. What's your point? Have you written a program in Haskell and found it too hard?

Please think before you want to lecture me again about deductive and inductive reasoning. You sound condescending instead of clever.

I refuse to discuss this with you any further until you drop the sarcasm and answer this simple question: how fluent are you with Haskell? If you claim to have actual Haskell programming experience (tutorials don't count) I'll take your word for it, accept that you understand its trade-offs, and let you have whatever last word you want to have in this subject, and move on.

> - No, we were talking about safety, not convenience.

If you don't want to compare programs written for the same effort, then what? Should we compare Haskell programs written with more effort to bash programs written with less effort? That's a confounding variable!

For the programmer there is always an opportunity cost: an hour spent satisfying a type-checker is an hour that could have been spent testing. Which use of that hour would provide the greatest safety? That is an empirical question.

> Stop shifting the subject.

No, you keep shifting the subject when you claim that Haskell programs are safer in practice but you then run away to your wonderland, where time stands still and the problem of opportunity cost has been solved, where you "prove" whatever you like while detached from reality, and then return to pretend that your "proofs" are valid in practice!

> - No, this is not a case of No True Scotsman.

So... if Angus writes fromMaybe "", which is accepted by the Haskell compiler but deletes all my files, is he a Haskell programmer?

> - No, a programming language with additional safeties is logically safer than one without, all else being equal (i.e. if no other safeties get removed instead).

Oh, "logically"! It's amazing what you can "prove" when you postulate a magical language that stops the clock while you satisfy the type-checker! Unfortunately, on this planet, time waits for no man, and you must choose how you spend it. Which approach provides the greatest safety, for the same effort? That is an empirical question, and you still have no empirical evidence for your position.

> - No, Haskell programmers aren't smug fools who believe that because their programs compile then they must be correct, and therefore no additional testing or QA is necessary.

No, you just believe you don't need empirical evidence for empirical claims! :-/

> A type-checker enforcing some constraints automatically makes your language practically safer than one without it.

Perhaps. But perhaps the time spent satisfying a type-checker would be better spent testing. Perhaps bash is safer than Haskell in practice!

> perhaps the time spent satisfying a type-checker would be better spent testing

One of the reasons I like languages with more advanced types systems such as Haskell's or Scala's is because test suites in other languages to achieve the same code coverage take much longer to run.

> One of the reasons I like languages with more advanced types systems such as Haskell's or Scala's is because test suites in other languages to achieve the same code coverage take much longer to run.

Do you mean Haskell has better runtime performance than dynamic languages, test for test, or that programs in dynamic languages need more tests (say, tests of function return types), or both?

In practice programs are written by programmers, not generated randomly, so it is not necessary to test "all the things that can go wrong" but only the things that programmers actually do wrong in practice.

With your reasoning bugs would have just stopped existing altogether decades ago.

Obviously they haven't.

Suppose a function f(a, b) should return the sum of its arguments (i.e. a + b). What tests would you write for this function?

So you refused to answer my direct question: how fluent are you with Haskell? I must assume the answer is "not much", which is why you keep building strawmen and disregarding everything people tell you about the language.

For an empirical advocate, you keep arguing from a quite theoretical point of view.

Good luck with that!

> So you refused to answer my direct question: how fluent are you with Haskell?

http://www.paulgraham.com/disagree.html

    DH0
    DH1 <-- you are here
    DH2
    DH3
    DH4
    DH5
    DH6

> For an empirical advocate, you keep arguing from a quite theoretical point of view.

What you assert without evidence can be dismissed without evidence.

Sooo... how fluent are you with Haskell?

> So... if Angus writes fromMaybe "", which is accepted by the Haskell compiler but deletes all my files, is he a Haskell programmer?

He is a Haskell programmer, the same as any Haskell programmer that runs launchAllNukes. What he is not is a surprised Haskell programmer, unlike someone, say, a programmer using bash or a programming language which allows nulls and/or accessing undefined variables with surprising results.

Why is Angus not surprised? Well, because he chose to return "" when he had Nothing. Presumably he thought the empty string was an acceptable value, and he wasn't trying to indicate "no value", because that is what Haskell programmers use Maybe for (and please don't mention Scotsmen here, because it will only make you seem ignorant). If his choice turned out to cause a bug, he made a mistake. But note this is unlike the situation for Mr Bash, who didn't choose to access an undefined variable, and unlike Mr Java Dev, who didn't choose to ignore a possible null return value. This is because Haskell is safer than bash or Java: Angus, Mr Bash and Mr Java can all make mistakes when choosing default values, but unlike the other two, Angus cannot make the mistake of accessing an uninitialized variable or a null reference. He is lucky like that!

> Yes, and perhaps the bash programmer could likely eliminate that fault through testing, perhaps about as likely as the Haskell programmer could get the Haskell compiler to accept a program at all!

Testing all the things that can go wrong in a bash script is much more difficult than getting a Haskell compiler to accept a program.

Ok, so 50%, 95%--whatever your number is--of the code in Haskell we have established is susceptible to dramatically fewer bugs than any other language out there. How can you possibly claim it doesn't matter? Just because you can construct a situation where it seems to not matter doesn't mean that situation is representative.

And oh by the way, we can easily prevent your situation in Haskell as well.

    safeRm :: SafeFilePath -> IO ()

Then we create the SafeFilePath data type (it can even be a newtype, which means it will have zero performance overhead) and we can write a smart constructor that makes it impossible to ever have dollar signs, stars, or anything else that might cause this kind of bug.

    mkSafeRm :: String -> Maybe SafeFilePath

Then you hide that stuff away in a module and only expose a safe interface. Now, BOOM, safeRm cannot possibly ever have the bug you described. This is made possible by purity, strong static types, and the module system. Some mainstream languages allow you to partly achieve this, but it usually incurs lots of boilerplate and the lack of immutability means that there will be more holes in whatever solution you can come up with.

> 95% [...] of the code in Haskell we have established is susceptible to dramatically fewer bugs than any other language out there.

No! Haskell has about the same proportion of LOC performing IO as any language. In Haskell, it may be easier to find where the IO code is, using the type system, but that doesn't make any of the code correct.

> Then you hide that stuff away in a module and only expose a safe interface.

You could do that in any language.

I think you are talking past each other.

Indeed Haskell does not automatically make code higher quality than any other language.

On the other hand, Haskell provides more infrastructure for making code reliable than most (or maybe all) mainstream languages.

Did you read the thread? :-p

> Haskell provides more infrastructure for making code reliable than most (or maybe all) mainstream languages.

Is there any empirical evidence that Haskell programs really are more reliable (all else being equal)? Is all that infrastructure actually useful?

Now you're not even listening to what I said. In my topmost post in this thread I showed how pure code in Haskell is susceptible to dramatically fewer potential bugs than equivalent code in any other mainstream language.

I said:

> There are no other possibilities, period.

And you agreed:

> That's true!

Most of that bug reduction was made possible by Haskell's purity/immutability. Now you're completely ignoring that point that we already established.

> In Haskell, it may be easier to find where the IO code is, using the type system, but that doesn't make any of the code correct.

No, it doesn't deductively "make any of the code more correct". It makes the code inductively "more likely to be correct". You asked for empirical evidence for the inductive claim and I gave it to you.

> You could do that in any language.

No, you could not. Other languages have module systems with hiding, but they do not have purity, the ability to categorically eliminate things like null errors, etc. You're zooming in to one feature, but it's not just one feature that enables all this. It's the combination of several.

> And you agreed:

I did agree that you can prove some properties about your code. Specifically, you can prove which parts of the code do not perform IO, and in that limited sense "if it compiles, it works" for that example, but that does not hold in general.

I did not agree that your code is more likely to be correct in general. The non-IO code may still be wrong (as you said then: it could return the first element of the list instead of the last one) and the IO code may also be wrong. And you have no evidence that any of that code is more likely to be correct.

The Haskell compiler can enforce some organization on your code (IO code goes here, non-IO code goes there) but the bugs could still be anywhere. All you have done is to shift the deckchairs on the Titanic!

> Most of that bug reduction was made possible by Haskell's purity/immutability.

You have no evidence of any actual bug reduction.

> You asked for empirical evidence for the inductive claim and I gave it to you.

Working deductively from the definition of Haskell is not empirical evidence for the claim that Haskell programs are more likely to be correct.

> And you have no evidence that any of that code is more likely to be correct.

> You have no evidence of any actual bug reduction.

> Working deductively from the definition of Haskell is not empirical evidence for the claim that Haskell programs are more likely to be correct.

My deductive reasoning is not the evidence I'm citing here. We counted the total number of ways that a function could go wrong and saw that in pure Haskell code, the number is drastically reduced. We know that the bug types we eliminated actually occur in practice, so under the reasonable assumption that the distribution of bug types is relatively constant, those numbers do provide empirical evidence (observational, not experimental) that Haskell programs are more likely to be correct.

Yes, pure code can still be wrong, but it can be wrong in a lot less ways than the impure code that you're stuck with in other languages. That code is still doing useful work that is also bug-prone in other languages. Therefore we can be reasonably confident that it will reduce bugs.

If you absolutely insist on experimental evidence, we have that too: https://www.youtube.com/watch?v=BveDrw9CwEg#t=1207

> My deductive reasoning is not the evidence I'm citing here.

You have no evidence, only (invalid) deductions.

> We counted the total number of ways that a function could go wrong

If you did this it would be deduction.

> and saw that in pure Haskell code, the number is drastically reduced.

No.

Say you have an IO function with two parts, a non-IO part to compute a directory name using some input, and an IO part to remove that directory:

    rmrf_steamroot some_input =
        -- some code to compute a directory name using some_input
        ...
        -- some code to remove that directory
        ...

Now, the first part does not perform IO, so let's extract that into a non-IO function:

    compute_directory_name some_input =
        -- some code to compute a directory name using some_input
        ...

    rmrf_steamroot some_input =
        let directory_name = compute_directory_name some_input
        -- some code to remove that directory
        ...

How many bugs were removed by doing this? None. It's the same code, just moved about a bit.

Sure, the code in the non-IO function "compute_directory_name" does not perform IO (and therefore does not have IO bugs) but that code did not perform IO (and therefore did not have IO bugs) when it was in the original IO function "rmrf_steamroot"! So there is no bug reduction.

> those numbers do provide empirical evidence (observational, not experimental)

That is not empirical evidence. Perhaps it may help you to read this introduction to the topic:

    https://en.wikipedia.org/wiki/Empirical_evidence

(And where it says "observation or experimentation" it may help if you follow those links.)

> If you absolutely insist on experimental evidence, we have that too

As you said earlier, they "rewrote a substantial groovy app in Haskell". There are too many confounding variables there.

> Say you have an IO function with two parts

We're not even arguing about the same thing. I wasn't talking about the rm function, I was talking about the "last" function in my original comment.

> If you did this it would be deduction.

I did enumerate every possible way that function can go wrong in Haskell. It is precisely n-1 where n is the length of the list (we can ignore the empty list case without loss of generality because it is easy to handle that case statically). In every other language in mainstream use today, the number of ways it could go wrong is infinite. And we actually do see those happen sometimes in practice.

The analysis in the above paragraph is the "active acquisition of information from a primary source", i.e. observational evidence for the inductive argument that code written in Haskell is "more likely to be correct".

> As you said earlier, they "rewrote a substantial groovy app in Haskell". There are too many confounding variables there.

I'm keenly aware of the confounding variables. But the fact is, you're never going to find a significant study that doesn't have a bunch of confounding variables. If that's your criteria for making a decision in this domain, then you won't be accomplishing much. In fact, I doubt we even have strong experimental evidence that C is more productive than assembly language. If you have different people write the different languages, the skill of the people is a confounding variable. If you have the same person write them all, then their knowledge of the languages and their mounting domain experience are confounding variables.

So we take whatever evidence we can get. If my bayesian prior was that all languages are equally likely to result in correct programs, then this evidence tips the scale slightly in Haskell's favor. We can't take it to the bank yet, but we've only looked at a couple pieces of evidence. (That's not the only evidence out there, but I'm constraining the discussion to this because of the bandwidth of this communication channel.) Point is, I think we're at the point where savvy forward-looking people should at least take note of Haskell's potential benefits. However much we know now, we will continue to learn more as we observe more and more people using Haskell to build real things.

> I was talking about the "last" function in my original comment.

Then let's say that "some_input" is a list and the non-IO function "compute_directory_name" should return the last element of that list. If that code were instead a part of the IO function "rmrf_steamroot" then the code would have just as many bugs. Conversely, extracting code from an IO function into a non-IO function proves only that the code did not perform IO (and therefore did not have IO bugs) in the first place. There is no bug reduction.

> I did enumerate every possible way that function can go wrong in Haskell.

This is deduction.

> "active acquisition of information from a primary source"

Did you read beyond the first sentence of that article? "In living beings, observation employs the senses." Which senses did you use to deduce the number of ways a function can return an element of a list?

> i.e. observational evidence

No, a mathematical "observation" is not an empirical observation.

> So we take whatever evidence we can get.

We all do! But you have no evidence at all.

You are piecing a bunch of empirical facts together using reasoning, but there are lots of implicit assumptions in your reasoning.

One assumption is that reducing error cases, reduces errors. Maybe the other errors increase in prevalence when you reduce error cases?

You say that even in impure code you can factor out pure parts. You assume this refactoring doesn't introduce bugs.

You talk about the fraction of code that is pure in haskell repos. But we don't know how the amount of impure code compares to amount of impure code in other languages. Maybe it is the same? Just haskellers have some pure code in addition?

Finally, we are talking about the bug proneness of haskell, not just an idealized fp-language. Maybe something with haskell causes bugs. There are many candidates. Poor support for debugging has mentioned in another comment. Maybe the libraries are less mature. Maybe less IDE support. Maybe something about the syntax causes bugs. Etc etc.

For this reason I think it would be easier to just experimentally verify the hypothesis directly: Does Haskell cause less bugs?

> but there are lots of implicit assumptions in your reasoning.

Yes, there are assumptions, but now we're getting somewhere.

> One assumption is that reducing error cases, reduces errors. Maybe the other errors increase in prevalence when you reduce error cases?

I think this is pretty unlikely. If we switch from C to a programming language that makes buffer overflows impossible, we don't expect to see a corresponding increase in, for example, off-by-one errors. After working with a language like Haskell for awhile you start to see that when the compiler tells you about missing a case for Nothing, you don't just sweep it under the rug. You stop and think about that case. I think it's reasonable to assume that when a programmer stops and thinks about a case, he's more likely to get it right. Errors often happen because the programmer neglected to think about a case entirely.

> You say that even in impure code you can factor out pure parts. You assume this refactoring doesn't introduce bugs.

I'm not talking about refactoring here. I'm talking about writing your code that way from the start, so regressions aren't an issue. As for the question of how many bugs you might write to begin with, see the previous point.

> You talk about the fraction of code that is pure in haskell repos. But we don't know how the amount of impure code compares to amount of impure code in other languages. Maybe it is the same? Just haskellers have some pure code in addition?

In other languages ALL code is impure. There are no other pure languages in mainstream use today. So then the question becomes whether the pure code written in Haskell performs any useful function as opposed to being just meaningless fluff. It's obvious that this code performs tons of useful operations and every time it is used, we are avoiding the need to have to solve the same problem again. It's very clear what problems are solved by that code, and it's very clear that people are able to reuse it to avoid the work. Therefore, it's absolutely not simply additional cruft.

> Finally, we are talking about the bug proneness of haskell, not just an idealized fp-language. Maybe something with haskell causes bugs.

None of the points you mention cause bugs. Lack of debugging has nothing to do with causing a bug. It just means that you'll have to go about fixing your bug differently. You can look for counter-arguments all day long, but at some point you're just grasping at straws.

> For this reason I think it would be easier to just experimentally verify the hypothesis directly: Does Haskell cause less bugs?

It's not easier. Building software is hard and takes a long time. Furthermore, constructing a scientifically valid experiment is even more costly. Most people want to be productive, so they're not going to go to that effort. There is huge variation between people, so these kinds of experiments have to be undertaken like medical studies...i.e. with large n. If you're interested in building complex, real-world systems, you're simply not going to get a large n. Also, Haskell has only become commercially viable in the last 5 or so years, so there hasn't yet been enough time/effort spent to perform these experiments.

But even with all these caveats, we do have some experimental evidence. There was a CUFP report from a company that rewrote a substantial groovy app in Haskell [1]. And the result is that yes, Haskell did indeed result in fewer bugs.

[1] https://www.youtube.com/watch?v=BveDrw9CwEg#t=1207

Groovy was originally designed as a scripting language intended for manipulating and testing classes written in a statically-typed language, Java, in which substantial apps should be written. Only later did new managers of Groovy start promoting it for building systems even though it wasn't suitable for that. A better test would be rewriting a substantial Java app in Haskell.

I really wish static typing advocates would consider making inductive claims. The last few times I've asked for such evidence the response has been along the lines of "you just don't understand". It's indicative of a general intellectual orientation that I think has held back the introduction of valuable PLT concepts into mainstream languages.

> You have proved the original (deductive) claim "if it compiles, it works" for that one specific example, but that does not hold in general.

Are you sure it does not hold in general? Upon repeating mightybytes example with all Haskell functions vs another language I feel like you'd get similar results due to pervasive purity and the type system.

Actually, using a non-total function like last doesn't do your claims any favours. I'd have picked map as the canonical example for free theorems.

I chose that non-total function because it is easier to enumerate all the possible error cases than with the map function. And the error case is easily handled by the combination of incomplete pattern match and Safe Haskell. I was also trying to emphasize purity more than free theorems.

Oh, hey, I get to copypasta one of the citations from my Master's thesis. Yes, there is empirical evidence!

http://macbeth.cs.ucdavis.edu/lang_study.pdf

>Abstract:

>What is the effect of programming languages on software quality? This question has been a topic of much debate for a very long time. In this study, we gather a very large data set from GitHub (729 projects, 80 Million SLOC, 29,000 authors, 1.5 million commits, in 17 languages) in an attempt to shed some empirical light on this question. This reasonably large sample size allows us to use a mixed-methods approach, combining multiple regression modeling with visualization and text analytics, to study the effect of language features such as static v.s. dynamic typing, strong v.s. weak typing on software quality. By triangulating findings from different methods, and controlling for confounding effects such as team size, project size, and project history, we report that language design does have a significant, but modest effect on software quality. Most notably, it does appear that strong typing is modestly better than weak typing, and among functional languages, static typing is also somewhat better than dynamic typing. We also find that functional languages are somewhat better than procedural languages. It is worth noting that these modest effects arising from language design are overwhelmingly dominated by the process factors such as project size, team size, and commit size. However, we hasten to caution the reader that even these modest effects might quite possibly be due to other, intangible process factors, e.g., the preference of certain personality types for functional, static and strongly typed languages.

> "I cannot say that getting upset over people using jokey memes to communicate ideas (Haskell is more likely to be correct after a successful type-check than other langs) is likely to do you much good."

You have, evidently, taken the least-charitable interpretation of GP's post yourself. And, right in the context of a discussion where you were the person to introduce that phrase!

The context I've read that remark in before is discounting the need for automated testing. At least one example has been provided in this thread of a Haskell developer claiming to have released code after it was verified by the type checker but without actually testing it. I don't think it's reasonable to take the phrase at anything but face value, considering that it's used as a promotional slogan by Haskellers.

"misleading claims like "if it compiles it works.""

ML family of languages contain powerful language features and libraries that, when programmed using particular style, can produce programs that actually do that (if they are brief). They are not magic, the point is just that the abstractions used there effectively remove large categories of typical bugs. Of course the language itself is not sufficient, one must study how programs are supposed to be written in the said languages to understand the utilization of those features.

Yaron Minsky's "Ocaml for the masses" in http://queue.acm.org/detail.cfm?id=2038036 explains this far more better than I could.

The claim "If it compiles, it works" taken literally is so trivially falsifiable that it cannot reasonably be interpreted as a serious claim that types "solve all correctness problems".

EDIT: I propose that next time you read "If it compiles, it works" you reply with "Are you suggesting that types solve all correctness problems?" I guarantee you that you will not get an affirmative response.

EDIT: I do however take the point that fans of strongly typed programming should act to moderate the excitement of some amongst their numbers in order to reduce the incidence of ambigous or misleading claims.

I've always taken it as meaning, "If it compiles, it must works, otherwise you're in trouble;" given that debuggers for Haskell are still relatively immature (especially for its age), your best bet is to lean heavily on the type system.

You can still run tests. Debuggers are great for figuring out why your program is wrong and how to fix it. But they seldom alert you to problems in the first place. Tests do.

Undoubtedly--tests, static types, debugging--I want them all!

This is a Haskell-specific problem. OCaml has an excellent debugger, not to speak of F#.

OCaml and F# are also more conventional. Lazy evaluation is a pain during debugging; even using laziness in a language like C# can be troublesome when you hit the debugger. So if you are going to rely on a lot of it, might as well have a lot of static typing to avoid debugging it.

If the program is a composed from trivial data conversion steps that are implementable using standard transforms (C++:s stl algorithms, ML:s folds, etc) then it is very likely that it works when it compiles. If there are various branches in the logic and I can encode those branches using types as invariants then that eliminates a particular category of bugs altogether which reduces logical errors. If I use immutable variables it helps even more. I'd say the 'compiles and works' means that if one can leverage existing operations on containers and use types as helpfull invariants then those two stylistic choices reduce the possible number of bugs in various categories.

I would not claim all errors are removed... e.g. numeric code that depends on the precision of arithmetic on floating points is as error prone with or without static types.

I can confirm that "If it compiles, it works" is tongue in cheek.

However, it's also true that I feel confident that a program in OCaml will be working correctly either the first time, or shortly afterwards, once it compiles (and, just as importantly, will keep working tomorrow or break at compile time). Knowing that the compiler eliminates for you a large amount of potential mistakes is a huge relief, and lets you focus on the parts of your program where the compiler cannot help you and where logic errors are lurking - especially where you are manipulating several values of the same type.

Most of the time, that's tongue-in-cheek.

On the other hand, when working with dependent types, the specification is a type, and if the theorem giving that specification type-checks (ie: the "proof" is a program of the appropriate type), then the code is correct, period.

Of course, attempting to prove the theorem can be hair-pullingly frustrating and takes valuable time, but it will expose the assumptions and corner-case you weren't thinking clearly about.

Reply on news.ycombinator.com