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

401–410 of 419 posts

Re: Correctness and composability bugs in the Julia ecosystem

#401

Post by cestith »

cb321 wrote: post #382
cestith wrote: post #372

Earlier quoted context omitted.

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..).

I've actually become somewhat interested in Hy lately. Having a Lisp that targets the Python AST may come in handy. If there was a Nim facility for full Lisp or a very Lispy syntax that could be really nice.

https://github.com/hylang/hy

Re: Correctness and composability bugs in the Julia ecosystem

#402

Post by jolux »

pron wrote: post #400
jolux wrote: post #391

Earlier quoted context omitted.

> 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 "factu…

> That is the difference between fact and conjecture.

Yes, but I'm trying to make a formal statement of fact here, not an empirical one.

> 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.

Here I am attempting to make a formal statement about the set of runtime behaviors that can be exhibited under static type systems. What I'm saying is that there is a set of incorrect runtime behaviors that can only be exhibited in a dynamic type system, that is, the set of type errors. I'm not aware of any runtime errors that can only be exhibited under a static type system. I'm not well educated enough in the relevant fields to be able to formalize this with notation (I would do so if I was, I think notation communicates these things much more clearly than words) but I do believe it has a formal representation.

> A conjecture that we've tried to verify yet failed to see a large effect is a problematic conjecture.

I think we're somewhat talking past each other here. What I'm saying is that the set of possible incorrect runtime behaviors is smaller in a static language. This can't really be empirically verified, it should have a formal answer in type theory or programming language theory. It's possible I'm wrong about what the formal answer is, but I haven't seen you address it yet. It's also possible that this is true but not strongly related to the way that bugs evolve in typical software engineering practice, I've speculated upthread that the total number of bugs might be similar because programmers make a higher number of repeated mistakes from the more narrow set while programming in static languages (though personally this seems unlikely). It's further possible that this is just not a very significant effect, as you have conjectured. However it is my belief that if there is an effect on bugs overall that it derives from what I understand to be a formal character of the runtime behavior of statically typed programs, that there are fewer ways for them to "go wrong."

Re: Correctness and composability bugs in the Julia ecosystem

#403

Post by adgjlsfhk1 »

Const-me wrote: post #397
adgjlsfhk1 wrote: post #146

Earlier quoted context omitted.

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 ) ); }

2 problems: Julia supports cpus without FMA, and on windows, llvm will use libc to constant fold the value of fma even on computers that have fma in hardware.

Re: Correctness and composability bugs in the Julia ecosystem

#404

Post by Const-me »

adgjlsfhk1 wrote: post #403
Const-me wrote: post #397

Earlier quoted context omitted.

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 ) ); }

2 problems: Julia supports cpus without FMA, and on windows, llvm will use libc to constant fold the value of fma even on computers that have fma in hardware.

Hardware requirements are up to the product management. For instance, many modern videogames (they generally want compatibility because directly translates to sales) no longer support 32-bit or pre-AVX1 processors. Technically, Julia can drop the support of pre-FMA3 processors if it helps moving forward.

It’s inevitable anyway due to the changing hardware requirements of the OS, the only question is “when”. I don’t think Windows 10 21H2 supports any CPU which doesn’t have SSE 4.1, it’s only a matter of time when Windows will require support of newer instruction sets.

About LLVM, can’t they compile that thing with an option like -mfma to use hardware FMA3 for constant folding?

Re: Correctness and composability bugs in the Julia ecosystem

#405

Post by Tainnor »

pron wrote: post #399
Tainnor wrote: post #392

Earlier quoted context omitted.

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 assertio…

I think you're guilty yourself of what you're accusing other people of.

I haven't seen people ITT arguing that there is empirical evidence for types providing better correctness guarantees, just that they strongly believe it to be the case given their own experience.

Re: Correctness and composability bugs in the Julia ecosystem

#406

Post by nancarrow »

jolux wrote: post #259
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…

> Note that Matlab, the workhorse of scientific computing for a few decades now, is even less typed than Julia. You always make this argument when discussing PL features and I find it irksome. People get along fine without this feature, therefore there’s no sense in implementing it. But it cuts the other way, or we’d all still be using assembly. How many Matlab users know things could be better? Was the superiority o…

> How many Matlab users know things could be better?

not very many in my experience - matlab rots the brain

Re: Correctness and composability bugs in the Julia ecosystem

#407

Post by [deleted] »

ChrisRackauckas wrote: post #306
patrickkidger wrote: post #231

Earlier quoted context omitted.

FWIW my take is not that Yuri is expressing "there are too many bugs" so much as he's expressing a problem in the culture surrounding Julia itself: > But systemic problems like this can rarely be solved from the bottom up, and my sense is that the project leadership does not agree that there is a serious correctness problem. Concisely: 1. The ecosystem is poorly put together. (It's been produced by academics rather t…

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…

[deleted]

Re: Correctness and composability bugs in the Julia ecosystem

#408

Post by wmoses »

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…

Enzyme dev here, so take everything I say as being a bit biased:

While, by design Enzyme is able to run very fast by operating within the compiler (see https://proceedings.neurips.cc/paper/2020/file/9332c513ef44b... for details) -- it aggressively prioritizes correctness. Of course that doesn't mean that there aren't bugs (we're only human and its a large codebase [https://github.com/EnzymeAD/Enzyme], especially if you're trying out newly-added features).

Notably, this is where the current rough edges for Julia users are -- Enzyme will throw an error saying it couldn't prove correctness, rather than running (there is a flag for "making a best guess, but that's off by default"). The exception to this is garbage collection, for which you can either run a static analysis, or stick to the "officially supported" subset of Julia that Enzyme specifies.

Incidentally, this is also where being a cross-language tool is really nice -- namely we can see edge cases/bug reports from any LLVM-based language (C/C++, Fortran, Swift, Rust, Python, Julia, etc). So far the biggest code we've handled (and verified correctness for) was O(1million) lines of LLVM from some C++ template hell.

I will also add that while I absolutely love (and will do everything I can to support) Enzyme being used throughout arbitrary Julia code: in addition to exposing a nice user-facing interface for custom rules in the Enzyme Julia bindings like Chris mentioned, some Julia-specific features (such as full garbage collection support) also need handling in Enzyme.jl, before Enzyme can be considered an "all Julia AD" framework. We are of course working on all of these things (and the more the merrier), but there's only a finite amount of time in the day. [^]

[^] Incidentally, this is in contrast to say C++/Fortran/Swift/etc, where Enzyme has much closer to whole-language coverage than Julia -- this isn't anything against GC/Julia/etc, but we just have things on our todo list.

[ps sorry if this ended up as a dup, I meant to reply deeper in the tree, so I deleted the older comment and moved it here].

Re: Correctness and composability bugs in the Julia ecosystem

#409

Post by btilly »

wmoses wrote: post #408
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…

Enzyme dev here, so take everything I say as being a bit biased: While, by design Enzyme is able to run very fast by operating within the compiler (see https://proceedings.neurips.cc/paper/2020/file/9332c513ef44b ... for details) -- it aggressively prioritizes correctness. Of course that doesn't mean that there aren't bugs (we're only human and its a large codebase [ https://github.com/EnzymeAD/Enzyme ], especially i…

With luck you will succeed. And that is a great thing.

But I maintain my position. If users are choosing packages because of speed without worrying about correctness, then packages will become popular that care less about correctness than what you describe. And when people combine popular packages that make conflicting assumptions, correctness will be lost.

In other words the problem is the attitude, not the specific package. For another example of the same problem, look at how C/C++ compilers prioritizing speed has resulted in their taking advantage of undefined behavior in a way that makes it far harder for any significant C/C++ codebase to be correct.

Re: Correctness and composability bugs in the Julia ecosystem

#410

Post by garrison »

Similar correctness issues are a big part of the reason that, several years ago, I submitted a series of pull requests to Julia so that its entire test suite would run without memory errors under Valgrind, save for a few that either (i) we understood and wrote suppressions for, or (ii) we did not understand and had open issues for. Unfortunately, no one ever integrated Valgrind into the CI system, so the test suite no longer fully runs under it, last time I checked. (The test suite took nearly a day to run under Valgrind on a fast desktop machine when it worked, so is infeasible for every pull request, but could be done periodically, e.g. once every few days.)

Even a revived effort on getting core Julia tests to pass under Valgrind would not do much to help catch correctness bugs due to composing different packages in the ecosystem. For that, running in testing with `--check-bounds=yes` is probably a better solution, and much quicker to execute as well. (see e.g. https://github.com/JuliaArrays/OffsetArrays.jl/issues/282)

Post reply on HN