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

381–390 of 419 posts

Re: Correctness and composability bugs in the Julia ecosystem

#381

Post by adgjlsfhk1 »

jolux wrote: post #380
pron wrote: post #373

Earlier quoted context omitted.

> These things are hard to study by their nature. Small effects are hard to study by their nature. Big effects are usually easy to spot. > there are a lot of programmers who feel quite strongly that static types reduce bugs There are a lot of people who feel quite strongly that homeopathy cures all kinds of diseases, but they've failed to demonstrate that. > But it’s clear that you accept other practices as beneficia…

> There are a lot of people who feel quite strongly that homeopathy cures all kinds of diseases, but they've failed to demonstrate that. This is a really poor comparison. How many people who know enough to judge these things believe that? I can understand that you’re rigorous in the empirical claims you accept here, but surely you can see that experienced software developers have somewhat more basis to make claims ab…

The extra bugs in a statically typed program go in the duplicated code that someone copied and changed the type names on because their type system wasn't flexible enough to let different types share the same code. This means that 3 years later when someone fixed a bug in part of the code, the bug remained in the other copy because the person writing the fix didn't know about the copy.

For a simple example, consider Arrow.jl vs the C++ implementation of the Arrow format. The Julia implementation is roughly 1/10th the lines of code (with more functionality), so even if there are 5x more bugs per line, the code still has fewer bugs.

Static types definitely reduce bugs per line, but they can still increase bugs per functionality.

Re: Correctness and composability bugs in the Julia ecosystem

#382

Post by cb321 »

cestith wrote: post #372
cb321 wrote: post #214

Earlier quoted context omitted.

Or Nim [1]..kind of an Ada with Lisp macros and more Pythonesque surface syntax. All three are ahead-of-time compiled/less REPL friendly than Julia, though. Taking more than 100 milliseconds to compile can be a deal breaker for some, especially in exploratory data analysis/science settings where the mindset is "try out this idea..no wait, this one..oops, I forgot a -1" and so on. In my experience, it's unfortunately…

The Python-like syntax is a minus for me. I didn't care for semantic leading whitespace in ABC. I don't care for it in Python. I therefore doubt I'd care for it in Nim. If that's your thing, an Ada with Lisp-like macros sounds delightful.

It is definitely more possible in Nim than in Python to use parens () in many (but not all) places to be more like bracy languages (but with parens being the brace..).

Re: Correctness and composability bugs in the Julia ecosystem

#383

Post by jolux »

adgjlsfhk1 wrote: post #381
jolux wrote: post #380

Earlier quoted context omitted.

> There are a lot of people who feel quite strongly that homeopathy cures all kinds of diseases, but they've failed to demonstrate that. This is a really poor comparison. How many people who know enough to judge these things believe that? I can understand that you’re rigorous in the empirical claims you accept here, but surely you can see that experienced software developers have somewhat more basis to make claims ab…

The extra bugs in a statically typed program go in the duplicated code that someone copied and changed the type names on because their type system wasn't flexible enough to let different types share the same code. This means that 3 years later when someone fixed a bug in part of the code, the bug remained in the other copy because the person writing the fix didn't know about the copy. For a simple example, consider A…

But there are plenty of static type systems that let different types share the same code, the problem you describe only exists in nominal type systems (like C++) as far as I know. With structural types like in TypeScript or Go you can express this trivially.

For that matter you can do this with subtype polymorphism in most cases. In Rust you can do it with trait objects as long as you control either the type or the trait. Probably there’s a way to do it in C++ too.

Re: Correctness and composability bugs in the Julia ecosystem

#384

Post by Sporktacular »

adgjlsfhk1 wrote: post #151
cbkeller wrote: post #145

Earlier quoted context omitted.

I actually wouldn't be surprised if the total number of tests run in the Julia ecosystem wasn't too different (thousands of packages with typically hundreds to thousands of unit tests, run on every commit and PR) -- virtually every Julia package has CI set up (at least standalone unit tests, though many packages could use more integration tests). Of course, in neither Matlab nor Julia do tests guarantee correctness.

sample size of 1, but I've run 1 billion tests today in Julia (floating point power for Float16, Float32 and Float64)

For correctness? What was the result?

Re: Correctness and composability bugs in the Julia ecosystem

#385

Post by pron »

jolux wrote: post #380
pron wrote: post #373

Earlier quoted context omitted.

> These things are hard to study by their nature. Small effects are hard to study by their nature. Big effects are usually easy to spot. > there are a lot of programmers who feel quite strongly that static types reduce bugs There are a lot of people who feel quite strongly that homeopathy cures all kinds of diseases, but they've failed to demonstrate that. > But it’s clear that you accept other practices as beneficia…

> There are a lot of people who feel quite strongly that homeopathy cures all kinds of diseases, but they've failed to demonstrate that. This is a really poor comparison. How many people who know enough to judge these things believe that? I can understand that you’re rigorous in the empirical claims you accept here, but surely you can see that experienced software developers have somewhat more basis to make claims ab…

> but surely you can see that experienced software developers have somewhat more basis to make claims about type systems

But experienced software developers, more than "random people", should know that if they make a conjecture, it's tested and isn't verified, they should reconsider their conjecture.

> You mentioned the TypeScript study, it’s not like there’s no evidence for believing this like there is with homeopathy.

There is no evidence for believing this. If you believe the evidence for TS vs JS in particular, then you should also believe the failure to find a more general effect.

> I mean, how could they not?

That's an interesting question and there are many answers; I've been interested in the complex subject of software correctness for years, and have written a bit about it (https://pron.github.io/). The more you study software correctness, the more you learn how complicated it is and that there are no easy answers. In particular, you learn that it's not true that more soundness is always a good path toward more correctness. But if you accept your preconceived notions over empirical study, then there's little hope for making actual progress.

> Where are those bugs in a statically typed program, if they haven’t been eliminated?

I gave you an example of where they are. If you want to go down the path of thinking about the theory of software correctness, start by convincing yourself that for every JavaScript program there is a Haskell program (perhaps living entirely inside an Either monad) that behaves the same way.

Re: Correctness and composability bugs in the Julia ecosystem

#386

Post by Tainnor »

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…

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 use of reflection, the effect dissipates... and so on (these are just examples for potential confounders, I'm not claiming they're true).

You are correct that one cannot claim that "static typing leads to fewer bugs" is a demonstrably correct statement, but I don't think you can claim that there demonstrably can be no (big) effect either. And in the end, you're also allowed to believe in conjectures even when there is no solid evidence behind it. People do that all the time, even scientists.

Re: Correctness and composability bugs in the Julia ecosystem

#387

Post by jolux »

pron wrote: post #385
jolux wrote: post #380

Earlier quoted context omitted.

> There are a lot of people who feel quite strongly that homeopathy cures all kinds of diseases, but they've failed to demonstrate that. This is a really poor comparison. How many people who know enough to judge these things believe that? I can understand that you’re rigorous in the empirical claims you accept here, but surely you can see that experienced software developers have somewhat more basis to make claims ab…

> but surely you can see that experienced software developers have somewhat more basis to make claims about type systems But experienced software developers, more than "random people", should know that if they make a conjecture, it's tested and isn't verified, they should reconsider their conjecture. > You mentioned the TypeScript study, it’s not like there’s no evidence for believing this like there is with homeopat…

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 is always a good path toward more correctness.

I’m still curious what definition of “correctness” you’re using here. Formal correctness? Bugs per line of code? Generally I’m thinking in terms of formal correctness, in which case I think it’s basically a truism that more soundness leads to more correctness. At some cost, perhaps.

> I gave you an example of where they are.

Yes, but those bugs are not unique to static languages, and I’ve never claimed that static languages eliminate all kinds of bugs. As far as I could tell from reading the study, it’s not evidence that static languages encourage this sort of bug more.

To be blunt: I think the set of kinds of bugs that can be written in dynamic languages is a strict superset of the kinds of bugs that can be written in a static language. Maybe I’m completely wrong about this! But this is the root of my reasoning.

Re: Correctness and composability bugs in the Julia ecosystem

#388

Post by josephg »

cbkeller wrote: post #377
jrochkind1 wrote: post #376

Earlier quoted context omitted.

Right, it's a caveat to testing in general that shows "well, just write integration tests, it's not especially hard to do" is not a satisfactory solution to the problems discussed in OP with specific actually occuring examples. You were the one suggesting it was, not me!

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 is similar. By the time the borrow checker has sufficiently bruised my ego, my rust code often just works. And thats a joy.

What I'm hearing is that Julia is more like javascript and C, and less like typescript and rust. That in Julia you need to be more paranoid around correctness - because you can easily compile a binary that produces incorrect results. You need extensive integration tests to guard against that, because its not enough to know that two libraries work individually and compile together. They need to also be tested together or they might silently do the wrong thing.

That sounds like a bad experience. Honestly, that sounds worse than javascript. At least in javascript, type errors almost always result in instant crashes with a useful stack trace. You say testing Julia code isn't hard, but that doesn't mean I want to do it. Building a stone wall by hand isn't hard either, but I'll take my desk job every time.

Re: Correctness and composability bugs in the Julia ecosystem

#389

Post by pron »

Tainnor wrote: post #386
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…

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 favourite approach with something like, "I like it; maybe you'll like it, too", you make some unsupported assertion that goes like this: "you should use my thing because it will actually make an important contribution to some bottom-line effect you're interested in; oh, and by the way, you might not notice it." That isn't convincing at all, so it's best to stick with what we know: "I like it, maybe you'll like it, too."

Re: Correctness and composability bugs in the Julia ecosystem

#390

Post by pron »

jolux wrote: post #387
pron wrote: post #385

Earlier quoted context omitted.

> but surely you can see that experienced software developers have somewhat more basis to make claims about type systems But experienced software developers, more than "random people", should know that if they make a conjecture, it's tested and isn't verified, they should reconsider their conjecture. > You mentioned the TypeScript study, it’s not like there’s no evidence for believing this like there is with homeopat…

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 to more correctness. At some cost, perhaps.

And you'd be wrong, or, at least, the second part of your statement makes all the difference. What we want is the best correctness we can get for some given cost, or, given some effort, what should you do to get the most correct program? If you follow formal methods, some of the hottest lines of research right now are about reducing soundness to improve correctness.

> As far as I could tell from reading the study, it’s not evidence that static languages encourage this sort of bug more.

I didn't say they did. But you asked how we explain the observation that types don't improve correctness, and one explanation is that the kind of mistakes that types catch aren't the costliest bugs that make it to production, and perhaps the extra effort invested comes at the expense of other approaches that do uncover more serious bugs.

> But this is the root of my reasoning.

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

Post reply on HN