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

351–360 of 419 posts

Re: Correctness and composability bugs in the Julia ecosystem

#351

Post by patrickkidger »

btilly wrote: post #326
ChrisRackauckas wrote: post #306

Earlier quoted context omitted.

Lots of things are being rewritten. Remember we just released a new neural network library the other day, SimpleChains.jl, and showed that it gave about a 10x speed improvement on modern CPUs with multithreading enabled vs Jax Equinox (and 22x when AVX-512 is enabled) for smaller neural network and matrix-vector types of cases ( https://julialang.org/blog/2022/04/simple-chains/ ). Then there's Lux.jl fixing some majo…

The fact that things are being rewritten and the primary criteria being looked at is speed IS culturally a big part of the problem. If you don't prioritize provable correctness first, then I guarantee that the code is not correct. And as the complaint explains, incorrect code costs people months and leads them to not trust the result. Don't believe me? Re-read the blog post about how a major source of bugs is people…

100% this. In a discussion on "cultural correctness issues prevents me from using Julia", it's very telling that the response is "more speed!"

There's been a decent number of posts based around "Julia has these problems". And I don't think that's because the world at large has a vendetta; I think it's because the world at large desperately wants to use Julia, but struggle with hard blocks that are currently preventing adoption.

FWIW I do think there's a growing acceptance in the Julia community that these concerns are real, which is good. (See the parallel discussion on the Julia Discourse.)

Re: Correctness and composability bugs in the Julia ecosystem

#352

Post by JonChesterfield »

cleandreams wrote: post #334

Unfortunately this is not a feature but a bug, and the worst kind, a bug at the language design level: Basically, Julia tries very hard to make composability work, even if the authors of the packages that you're composing don't know anything about each other. That's a critical feature that makes Julia as powerful as it is, but of course you can easily end up with situations where one or the other package is making im…

It's an interesting point in the language design space. Composing unrelated projects gives a rapidly increasing state space of interactions which noone is directly responsible for. I can't decide if that's brilliant or broken by design.

Re: Correctness and composability bugs in the Julia ecosystem

#353

Post by dash2 »

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.

I assume you're not arguing that humans got it wrong to ever count from 1. So you must mean that when counting things, we start from 1 and when indexing we start from 0. Like, "that dog has 4 legs", but when you refer to them it's the "0th leg, 1st leg, 2nd leg and 3rd leg"? This seems weird. It's true that then the first - sorry, 0th - leg is 0 from the start of the array. But it also means that the last element of the array is one less than its size. You'd also struggle to do the operation of counting. You'd have to remember, am I indexing or counting?

If you say so! Maybe you should start a foundation to encourage humanity to change its counting behaviour. The effective altruists might throw you a couple of million.

Re: Correctness and composability bugs in the Julia ecosystem

#354

Post by ChrisRackauckas »

patrickkidger wrote: post #351
btilly wrote: post #326

Earlier quoted context omitted.

The fact that things are being rewritten and the primary criteria being looked at is speed IS culturally a big part of the problem. If you don't prioritize provable correctness first, then I guarantee that the code is not correct. And as the complaint explains, incorrect code costs people months and leads them to not trust the result. Don't believe me? Re-read the blog post about how a major source of bugs is people…

100% this. In a discussion on "cultural correctness issues prevents me from using Julia", it's very telling that the response is "more speed!" There's been a decent number of posts based around "Julia has these problems". And I don't think that's because the world at large has a vendetta; I think it's because the world at large desperately wants to use Julia, but struggle with hard blocks that are currently preventin…

Two of the mentioned packages, Lux and Enzyme, have increased correctness and decreased API surface... and were not mentioned for speed (though a lot of things end up faster when it's easier to prove correctness in the compiler)... so the response wasn't "more speed" but "here's correctness with resulting speed"...

Re: Correctness and composability bugs in the Julia ecosystem

#355

Post by pron »

riwsky wrote: post #322
pron wrote: post #296

Earlier quoted context omitted.

> I’ve definitely seen you argue along the lines of “it hasn’t been implemented in Java, therefore nobody uses it and we can’t tell if it’s a good idea or not” before. You have not seen me argue anything along those lines. I have, however, said the converse, that we try not to adopt features in Java until they've proven themselves elsewhere. > However, in terms of eliminating patterns which are literally never correc…

“Want B” is not the same as “B”. “Should do A” is not the same as “A”. The reverse of “types prevent certain kinds of bugs” would be that “all code which doesn’t suffer from those kinds of bugs is typed”, not “if you don’t want those bugs, use types”. The parent does not assume B->A; your actual disagreement with them is over whether A -> B implies A -is-the-most-effective-way-to—> B. I share your understanding of th…

Formalising natural language is tricky, but I believe "every PL that leads to more correct programs is typed" is either equivalent or stronger than "if you want a PL that leads to more correct programs it should be typed." It could be stronger if the latter phrasing takes measure into account (so a bit of fuzzy logic), meaning the possibility that other approaches also lead to more correct programs but not as well. Still, I contend that my formalisation is correct enough to demonstrate the logical error that even if types imply correctness (not substantiated by evidence), it does not follow that correctness implies types (even less supported by evidence).

Re: Correctness and composability bugs in the Julia ecosystem

#356

Post by HelloNurse »

KenoFischer wrote: post #108

So this one is a tough one for me, because Yuri has certainly spent significant time with Julia and I think he's a very competent programmer, so his criticism is certainly to be taken seriously and I'm sad to hear he ended up with a sour opinion. There's a lot of different issues mentioned in the post, so I'm not really sure what angle to best go at it from, but let me give it a shot anyway. I think there's a couple…

> there are a number of "flagship" applications that are really pushing the boundary of what Julia can do, but at the same time also need a disproportionate amount of attention.

Disproportionate effort is an obvious sign that hacks to keep such flagships seaworthy are prioritized over a good language and a good library.

> Basically, Julia tries very hard to make composability work, even if the authors of the packages that you're composing don't know anything about each other.

Typically, programming languages and libraries don't need to "try very hard" because they are designed to be safe and correct, at the cost of curbing ambitious features.

> not all implicit assumptions are easily capturable in interfaces. Perhaps there needs to be more explicit documentation around what combinations of packages are "supported".

Supporting useful "combinations of packages" isn't a desirable approach to language and library evolution. Implicit assumptions must disappear, either by becoming explicit or by becoming unnecessary; both ways represent genuine progress, not fruitless firefighting.

Re: Correctness and composability bugs in the Julia ecosystem

#357

Post by pron »

jolux wrote: post #318
pron wrote: post #296

Earlier quoted context omitted.

> I’ve definitely seen you argue along the lines of “it hasn’t been implemented in Java, therefore nobody uses it and we can’t tell if it’s a good idea or not” before. You have not seen me argue anything along those lines. I have, however, said the converse, that we try not to adopt features in Java until they've proven themselves elsewhere. > However, in terms of eliminating patterns which are literally never correc…

> You have not seen me argue anything along those lines. I have, however, said the converse, that we try not to adopt features in Java until they've proven themselves elsewhere. You’ve definitely argued that not enough software has been written in Haskell to know whether it’s the right tool for anything and whether strong types are actually a good idea. > But the implication is reveresed! From A => B, i.e. types prev…

> to know whether it’s the right tool for anything and whether strong types are actually a good idea.

Nope. I don't know what you mean by "a good idea", and I prefer typed languages myself (mostly for tooling support), but I do often point out that the claim that types improve correctness — let alone the claim that they do that better than other approaches — is an empirical claim that is not supported by empirical evidence (which, in fact, appears to contradict it).

Also, that there have been few programs written in Haskell, and that Haskell has failed to demonstrate that it leads to better correctness are both pretty basic facts.

> All of the solutions I know to these problems involve types.

I don't know what you mean by "solutions to these problems", but while we've not found a correlation between types and more correct programs, we have found correlations between code reviews and tests and more correct programs. Types might well be the solution to many things (e.g. automatic refactoring and jump-to-definition), but the empirical evidence we have suggests that increased correctness isn't one of them.

> Surely you’re not saying that optionals don’t eliminate null pointer dereferencing, are you?

Types certainly eliminate various kinds of errors, yet studies did not find that they reduce bugs (except in specific circumstances; for example, there was one study that reported that TypeScript has 15% fewer bugs than JavaScript).

Just to give you a sense for one reason that happens, we can take your example of Maybe types. A null pointer exception occurs when code assumes a reference can't be null, but is wrong to make the assumption. A Maybe type would force a test somewhere. But the question then, is, what do you do when the value is empty? A brilliant study on software correctness [1] found that most catastrophic crashes in distributed systems occur not because programmers fail to consider certain exceptional situations — in fact, the language forces them to consider those situtations — but because they frequently do the wrong thing when those situations occur.

[1]: https://www.usenix.org/system/files/conference/osdi14/osdi14...

Re: Correctness and composability bugs in the Julia ecosystem

#358

Post by pron »

ThenAsNow wrote: post #250
pron wrote: post #180

Earlier quoted context omitted.

> A language with static types would have made it easier to build correct software This claim is repeated often, but numerous attempts have failed to demonstrate that this is generally the case in practice (there have been a couple of studies showing an effect in very specific circumstances). Static types might indeed assist with correctness, but they are not the only thing that does, and in some situations they coul…

We can trade anecdotes on this topic, but I've written numerical code in OCaml and also Julia. The strictness of OCaml's type system is painful in a numerical context but for virtually all other things it is awesome to pass code into the interpreter/compiler and catch structural problems at compile-time rather than maybe at runtime. OCaml's type system is almost certainly not the right model for Julia but the ad-hoc…

"Awesome", i.e. more enjoyable for you, and "more correct", i.e. fewer bugs in production, are two very different things. I also prefer typed languages for the software I tend to write and find them more enjoyable, but that still doesn't make me claim that types lead to more correct software.

Re: Correctness and composability bugs in the Julia ecosystem

#359

Post by bayindirh »

btilly wrote: post #326
ChrisRackauckas wrote: post #306

Earlier quoted context omitted.

Lots of things are being rewritten. Remember we just released a new neural network library the other day, SimpleChains.jl, and showed that it gave about a 10x speed improvement on modern CPUs with multithreading enabled vs Jax Equinox (and 22x when AVX-512 is enabled) for smaller neural network and matrix-vector types of cases ( https://julialang.org/blog/2022/04/simple-chains/ ). Then there's Lux.jl fixing some majo…

The fact that things are being rewritten and the primary criteria being looked at is speed IS culturally a big part of the problem. If you don't prioritize provable correctness first, then I guarantee that the code is not correct. And as the complaint explains, incorrect code costs people months and leads them to not trust the result. Don't believe me? Re-read the blog post about how a major source of bugs is people…

In most cases, being fast is useless without being correct. Even approximate things like simulations depend on the programming language being deterministic and correct. Otherwise the math of approximation doesn't work out.

With my programmer hat, the first thing I care is not speed for most cases. Unless there's an explicit need for speed, I don't select the language I gonna use with respect to its performance, and I don't port a tool unless the speed becomes limiting.

It's important to make it run first, then make it fast. Otherwise, things go very wrong, very fast (pun intended).

Re: Correctness and composability bugs in the Julia ecosystem

#360

Post by jerome-jh »

rudellius wrote: post #328
Tarrosion wrote: post #323

Earlier quoted context omitted.

How has Python - almost surely the most successful and widely adopted scientific programming ecosystem - avoided the problems of #2? E.g. Python doesn't have static typing. Is it just that Python is so widely used there's institutional support for incredible linting and type check tools despite the lack of static typing? Or that much of the science/data ecosystem of Python is written in lower level statically typed l…

Julia heavily makes use of multiple dispatch among with other convenient type related features much more complex than Python, to a point where they are often abused and sometimes have uncaught edge cases. It makes the language very powerful but has its downsides. And to be fair to Python, static analysis has come a very long way and the CPython interpreter makes far fewer complex assumptions than the Julia compiler.…

Indeed Python is relatively simple language. It also adheres to the principle of least astonishment and dynamic types are used towards this goal. Finally it does not mind making large changes to the language.

With Python most of the time when you have an unexpected result with the language or a library it is often a matter of realizing "OK that's the way it works", and moving on with your work. The language and libraries strive so much to always return sensible results that they are fewer instances when you would call a behavior a bug.

Post reply on HN