Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Correctness and composability bugs in the Julia ecosystem

yuri.is

Post reply on HN
Print view View original

391–400 of 419 posts

Re: Correctness and composability bugs in the Julia ecosystem

#391

Post by jolux »

pron wrote: post #390
jolux wrote: post #387

Earlier quoted context omitted.

I don’t think the subject of software correctness in practice is itself well-studied enough to say conclusively that my conjecture is false. I think what can be said conclusively is that at scale people cannot write memory-safe code in an unsafe language or type-safe code in a dynamic language, but obviously these are not the only kinds of correctness. > In particular, you learn that it's not true that more soundness…

> I don’t think the subject of software correctness in practice is itself well-studied enough to say conclusively that my conjecture is false. I don't claim that. Given what we know, the likeliest explanation to the findings so far is that an effect, if it exists, is probably small. > Formal correctness? Bugs per line of code? Both would work. > in which case I think it’s basically a truism that more soundness leads…

> perhaps the extra effort invested comes at the expense of other approaches that do uncover more serious bugs

I guess in my experience the effort invested programming in a static language is really not that much higher than dynamic, and in some ways I find it less effortful. For example: pattern matching on a sum type, being sure that I’ve handled all the cases I want to. Is there good empirical research on this?

> That's as good a conjecture to start with as any, but it needs to be revised with findings.

I was attempting to make a factual statement, not a conjecture. If it is true that static types eliminate a class of errors, then type errors must be really cheap for static types not to be worth it on those grounds. My prior is that compiler errors are cheaper than runtime errors here.

Re: Correctness and composability bugs in the Julia ecosystem

#392

Post by Tainnor »

pron wrote: post #389
Tainnor wrote: post #386

Earlier quoted context omitted.

I'm not sure if that's true, even big effects can be hard to verify if there are significant confounders. For example, let's imagine that writing OCaml code really leads to fewer bugs than writing code in Lisp (to just choose two languages) but only after you've trained people in OCaml for ten years. Or maybe, technically Java leads to measurably fewer bugs than Ruby, but because most popular Java projects make heavy…

You can believe in such a conjectures, but it's wise to consider the more probable possiblity that if an effect hasn't been found, then it is likely small. Also, in the end it doesn't really matter, because the conjecture that's repeated as an assertion isn't said merely as a scientific claim, but as an attempt to convince. Companies are interested in some bottom line effect, and rather than trying to sell your favou…

Show me the companies that only ever implement policies that have shown to be effective in rigorous empirical studies.

Usually some person (or a group of people) is in charge of some decision and that person will make judgment calls based on their beliefs. This is no less true of programming techniques than it is of management styles, corporate strategy or anything else.

Your insistence that we may not have beliefs about the very things we work with daily, unless they're empirically verified, is IMHO frankly ridiculous.

Re: Correctness and composability bugs in the Julia ecosystem

#393

Post by ThenAsNow »

pron wrote: post #375
ThenAsNow wrote: post #366

Earlier quoted context omitted.

I am not familiar with the studies you are relying on to make the point that statically-typed languages have no significant difference in terms of number of bugs in production compared to dynamically-typed. Measuring such things is challenging, and the most useful measure may not be in terms of "bugs in production" but by a number of other measures, such as how long it takes to surface bugs after the code is accepted…

Anyone is allowed to prefer a programming style that suits their aesthetics and habits, and like that one over all others. Aesthetic preferences are a very valid way to choose your programming language — ultimately that's how we all pick our favourite languages — and there's no need to make up universal empirical claims to support our preferences. Here's a good talk to watch on the subject: https://youtu.be/ePCpq0AMy…

  Anyone is allowed to prefer a programming style that suits their aesthetics and habits, and like that one over all others. Aesthetic preferences are a very valid way to choose your programming language — ultimately that's how we all pick our favourite languages — and there's no need to make up universal empirical claims to support our preferences.
That's fine, but I'm not sure what it has to do with my comment as it was not about preferences based on aesthetics or habits.

Thanks for the links though.

  There's really no need to assert what is really a conjecture, let alone one that's been examined and has not been verified.
There's no unsupported conjecture in "it is strictly more rigorous to catch equivalent bugs through the interpreter/compiler than through testing or other runtime-dependent approaches."

  If you believe the conjecture is intrinsically hard to verify, you're conceding that you're only claiming a small effect at best (big effects are typically not hard to verify), and so there's even less justification for continuing to assert it.
It's easy to fall victim to the Robert McNamara fallacy, that if something isn't easy to measure its effect or importance is insignificant. Anyone looking back at U.S. defense and procurement policy from his era is free to observe the lack of real-world congruence with such thinking. The Dan Luu page you cited, more than anything else, seems to reinforce that the cited studies are hard to interpret for any rigorous conclusions or for validity of methodology.

This is why I did not make sweeping statements along the lines of "the majority of dynamically-typed software in production [no qualifier on what "production" means] would have fewer bugs if it were statically-typed" or the like.

Re: Correctness and composability bugs in the Julia ecosystem

#394

Post by cbkeller »

josephg wrote: post #388
cbkeller wrote: post #377

Earlier quoted context omitted.

Well I don't think it's hard any more than writing any other sort of test in a given language. That doesn't mean it doesn't require expertise in that language.

I used to love javascript. When people asked, I made a similar argument - that you need tests anyway, and if you're writing tests you'll spot any obvious typing bugs in your javascript code. I think I was wrong. Moving to typescript has been a revelation for me, because I find I need far fewer tests to make working code. (And my code so often just works as soon as it compiles!). I can code much more fearlessly. Rust…

I can appreciate that perspective for sure.

Just to make sure we're on the same page though, it's perhaps worth clarifying that this particular integration issue isn't something you have to worry about every time you use two packages together (far from it), it's only in the case where you're trying to use a custom type from one package (e.g., one which replaces base Arrays or base Numbers or such) in functions from another package.

Re: Correctness and composability bugs in the Julia ecosystem

#395

Post by mirekrusin »

buescher wrote: post #245
mirekrusin wrote: post #235

Earlier quoted context omitted.

66% python, 32% C - for cpython. 94% python, 5% C - for pypy.

cpython is the reference implementation and 32% means about 350,000 lines of code. My point stands.

So is glasgow haskell compiler or ocaml compiler - so what?

Re: Correctness and composability bugs in the Julia ecosystem

#396

Post by DNF2 »

IshKebab wrote: post #244
ModernMech wrote: post #229

Earlier quoted context omitted.

The reason why this 0 vs 1 based indexing debate is never resolved is because all of the arguments are subjective. You've claimed definitively that "humans got it wrong", but to back up this argument you've pointed to vague notions of "elegance" and "understandability". Even Dijkstra in his argument relies on a notion of "ugliness". All such arguments fall squarely in the realm of "preferences". Just think about what…

It's not subjective. The fundamental meaning of an index is "how far are we from the start of an array". The first element is 0 from the start of the array. If humans had got this right then we wouldn't be even having this discussion. Same for similar mistakes like Pi vs Tau, negative electrons. But the mistake is understandable given that we didn't even think of 0 for a long time.

No, this is not the fundamental meaning of an index, it is simply the interpretation that you are using to make it easier to deal with for you personally. In my opinion, the fundamental meaning of an index is a number referring to element number `n`, so that `a[1]` is the first element, etc. But I don't begrudge you your working definition.

For some reason, people who are used to 1-based indexing generally recognize that both interpretations are perfectly fine, and that each works well in different contexts. For some other reason, people used to 0-based indexing feel so intellectually superior that they are unable to see the other side of the argument.

Re: Correctness and composability bugs in the Julia ecosystem

#397

Post by Const-me »

adgjlsfhk1 wrote: post #146
KKKKkkkk1 wrote: post #101

Earlier quoted context omitted.

FMA can't be broken on Windows because FMA is implemented in hardware by Intel. What's broken is the compiler that Julia uses on Windows.

the problem is that LLVM will happily miscompile fma instructions by turning them into incorrect constants due to windows having a broken libm. This is a bug in C/C++, and I'm currently unaware of a language that has fma and a good compiler which gives correct fma results on Windows.

CPUs support these instructions for 9 years now. When ignoring these old CPUs, most languages and compilers are usually doing a good job. Example in C which does not depend on any library functions:

    double fma( double a, double b, double c )
    {
        __m128d av = _mm_set_sd( a );
        __m128d bv = _mm_set_sd( b );
        __m128d cv = _mm_set_sd( c );
        return _mm_cvtsd_f64( _mm_fmadd_sd( av, bv, cv ) );
    }

Re: Correctness and composability bugs in the Julia ecosystem

#398

Post by pron »

ThenAsNow wrote: post #393
pron wrote: post #375

Earlier quoted context omitted.

Anyone is allowed to prefer a programming style that suits their aesthetics and habits, and like that one over all others. Aesthetic preferences are a very valid way to choose your programming language — ultimately that's how we all pick our favourite languages — and there's no need to make up universal empirical claims to support our preferences. Here's a good talk to watch on the subject: https://youtu.be/ePCpq0AMy…

Anyone is allowed to prefer a programming style that suits their aesthetics and habits, and like that one over all others. Aesthetic preferences are a very valid way to choose your programming language — ultimately that's how we all pick our favourite languages — and there's no need to make up universal empirical claims to support our preferences. That's fine, but I'm not sure what it has to do with my comment as it…

> That's fine, but I'm not sure what it has to do with my comment as it was not about preferences based on aesthetics or habits.

Because you made the claim that "it is strictly more rigorous to catch equivalent bugs through the interpreter/compiler than through testing or other runtime-dependent approaches," but that claim was simply not found to be true.

> There's no unsupported conjecture in "it is strictly more rigorous to catch equivalent bugs through the interpreter/compiler than through testing or other runtime-dependent approaches."

There is, unless you define "more rigorous" in a tautological way. It does not seem to be the case that soundly enforcing constraints at compile time always leads to fewer bugs.

> It's easy to fall victim to the Robert McNamara fallacy, that if something isn't easy to measure its effect or importance is insignificant.

The statement, "you will have fewer bugs but won't be able to notice it," is unconvincing. For one, if you can't measure it, you can't keep asserting it. At best you can say you believe that to be the case. For another, we care about the effects we can see. If the effect doesn't have a noticeable impact, it doesn't really matter if it exists or not (and we haven't even been able to show that a large effect exists).

That the effect is small is still the likeliest explanation, but even if you have others, your conjecture is still conjecture until it is actually verified.

> The Dan Luu page you cited, more than anything else, seems to reinforce that the cited studies are hard to interpret for any rigorous conclusions or for validity of methodology.

It does support my main point that despite our attempts, we have not been able to show that types actually lead to significantly fewer bugs, i.e. that the approach is "more rigorous" in some useful sense.

Re: Correctness and composability bugs in the Julia ecosystem

#399

Post by pron »

Tainnor wrote: post #392
pron wrote: post #389

Earlier quoted context omitted.

You can believe in such a conjectures, but it's wise to consider the more probable possiblity that if an effect hasn't been found, then it is likely small. Also, in the end it doesn't really matter, because the conjecture that's repeated as an assertion isn't said merely as a scientific claim, but as an attempt to convince. Companies are interested in some bottom line effect, and rather than trying to sell your favou…

Show me the companies that only ever implement policies that have shown to be effective in rigorous empirical studies. Usually some person (or a group of people) is in charge of some decision and that person will make judgment calls based on their beliefs. This is no less true of programming techniques than it is of management styles, corporate strategy or anything else. Your insistence that we may not have beliefs a…

That's not my insistence at all. You can believe what you like. What you can't do is make empirical assertions that we've not been able to validate empirically.

Companies may adopt a technique based on empirical findings or anything else they like; most people choose a favourite programming language because they like working with it better. But the statement that types lead to fewer bugs is a very particular assertion that is simply unsupported by evidence. You may believe that using types reduces baldness and make your choices based on that, but it's still a conjecture/belief at best.

Re: Correctness and composability bugs in the Julia ecosystem

#400

Post by pron »

jolux wrote: post #391
pron wrote: post #390

Earlier quoted context omitted.

> I don’t think the subject of software correctness in practice is itself well-studied enough to say conclusively that my conjecture is false. I don't claim that. Given what we know, the likeliest explanation to the findings so far is that an effect, if it exists, is probably small. > Formal correctness? Bugs per line of code? Both would work. > in which case I think it’s basically a truism that more soundness leads…

> perhaps the extra effort invested comes at the expense of other approaches that do uncover more serious bugs I guess in my experience the effort invested programming in a static language is really not that much higher than dynamic, and in some ways I find it less effortful. For example: pattern matching on a sum type, being sure that I’ve handled all the cases I want to. Is there good empirical research on this? >…

Until it's been measured, a statement is a conjecture, not "factual." A conjecture that we've tried to verify yet failed to see a large effect is a problematic conjecture.

We don't have good empirical findings about many things, most likely because many effects are small at best. But it doesn't matter. You're can say that you still believe something despite failed attempts to measure it, but you can't see it's "factual." That is the difference between fact and conjecture.

Post reply on HN