9 ms·

> Everything has correctness issues somewhere. Yes but Julia is (yet another) dynamic language, presumably for "ease of use". A language with static types woul

> Everything has correctness issues somewhere. Yes but Julia is (yet another) dynamic language, presumably for "ease of use". A language with static types would have made it easier to build correct software (scientific code in e.g. OCaml and F# can look pretty good). Julia chose a path to maximize adoption at the expense of building a reliable ecosystem. Not all languages choose to make this trade-off.

pron 4y ago
> 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 could come at the expense of others. I.e., even if types were shown to significantly help with correctness, it does not follow that if you want correctness your best course would be to add types. Given empirical studies, the current working hypothesis should be that if static types do have a positive effect on correctness, it is a small one (if it were big, detecting it would have been easy). Note that Matlab, the workhorse of scientific computing for a few decades now, is even less typed than Julia. That's not to say that Julia doesn't suffer from too many correctness issues (I have no knowledge on the matter), but even if it does, there is little support for the claim that typing is the most effective solution.
- StefanKarpinski 4y ago
  In particular, not a single issue mentioned in this article would have been prevented by static type checking.
  - grumpyprole 4y ago
    This is not true. For example, the issue regarding custom index ranges causing silent data corruption (6 examples) could be fixed with static types. Look how many of the other bug reports contain the phrase "does not check for" or refer to specific primitive types.
    - adgjlsfhk1 4y ago
      it is only fixed with static typing and no generics (i.e. C/Fortran). If you have a generic array supertype, a statically typed language would let you write exactly the same bug.
      - grumpyprole 4y ago
        If one has a different type or trait for unusual and normal range indices, then the signature for the procedure that assumes indexing from 1 can be written to disallow other starting indices.
    - DNF2 4y ago
      How would static types help with that? Whether your indexing range starts with zero or one or something else isn't necessarily encoded in the type domain. `1:length(A)` is just a range of `Int`s.
      - grumpyprole 4y ago
        Why not encode the starting offset into the type domain? Or at least distinguish between normal and unusual. Then the function signature can restrict to 1-offset arrays if that is what it assumes internally.
        DNF2 4y ago
        That means disallowing indexing with integers, I presume? Since an integer can take the values 0 or 1 equally. And what about the other end of the array. Must every index be restricted by type to be located in the acceptable range?
        markkitti 4y ago
        If the function signature said `Array` rather than `AbstractArray`, then this code would have been fine. `Array` indexing starts at `1`. ``` julia> function f(A::Array) println(A[1:length(A)]) end f (generic function with 1 method) julia> f([1,2,3,4]) [1, 2, 3, 4] julia> f(OffsetArray(1:10, -1)) ERROR: MethodError: no method matching f(::OffsetVector{Int64, UnitRange{Int64}}) ``` You could prevent this problem using Julia's type system. The `AbstractArray` might have been too broad. Based on the chronology of the code that might not have been apparent. See other threads for details. Another way would be to treat `firstindex` as a trait and dispatch on that. ``` julia> f(A::AbstractArray) = f(A, Val(firstindex(A))) f (generic function with 1 method) julia> f(A::AbstractArray, firstindex::Val{1}) = println(A[1:length(A)]) f (generic function with 2 methods) julia> f(A::AbstractArray, firstindex::Val{T}) where T = error("Indexing for array does not start at 1") f (generic function with 3 methods) julia> f(A::AbstractArray, firstindex::Val{0}) = println("So you like 0-based indexing?") f (generic function with 4 methods) julia> f([1,2,3,4]) [1, 2, 3, 4] julia> using OffsetArrays julia> f(OffsetArray(1:10, 1)) ERROR: Indexing for array does not start at 1 Stacktrace: [1] error(s::String) @ Base .\error.jl:33 [2] f(A::OffsetVector{Int64, UnitRange{Int64}}, #unused#::Val{2}) @ Main .\REPL[5]:1 [3] f(A::OffsetVector{Int64, UnitRange{Int64}}) @ Main .\REPL[3]:1 [4] top-level scope @ REPL[9]:1 julia> f(OffsetArray(1:10, -1)) So you like 0-based indexing? ```
- ThenAsNow 4y ago
  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 typing/interface system Julia currently employs is at strong odds with compile-time correctness. There's almost certainly some middle ground to be discovered which might be unsound in a strict sense but pragmatically constrains code statically so there is high likelihood of having to go out of your way to pull the footgun trigger. You can see how little type annotations are used in practice in major Julia libraries. It should be integral to best practice in the language to specify some traits/constraints that arguments must satisfy to be semantically valid, but what you often see instead is a (potentially inscrutable) runtime error.
  - pron 4y ago
    "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.
    - ThenAsNow 4y ago
      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 by the interpreter/compiler, how much time is spent on writing the implementation vs. writing & running tests, how many bugs occur on major refactorings, etc. If you have citations for studies you like, I'm certainly interested. My use of colloquialism aside, it is strictly more rigorous to catch equivalent bugs through the interpreter/compiler than through testing or other runtime-dependent approaches. In my own experience, despite being a more experienced programmer in my Julia-writing phase than in my OCaml-writing phase, it takes much more time to surface bugs in my "running" Julia code than OCaml. The lack of determinism in surfacing these bugs does not suggest as much confidence in the Julia code. You could counter by saying I'm probably able to implement more functionality in Julia per unit of up-front development time than the equivalent development time in OCaml, which I'd probably have to concede, but that just highlights measuring these things in a directly-comparable way is not easy. In the physical engineering disciplines, we often have disagreements about the level of sophistication of physics-based models that should be used for design and analysis. It's very reminiscent of these static vs. dynamic typing discussions in software development. There isn't a "one size fits all" answer, but generally, the more complex and expensive the system, the more important the models incorporate greater physical fidelity. My analogous conclusion here is a lot of technical/numerical code is complex enough that more rigor enforced by the language would likely be the right tradeoff for a net win on up-front correctness (vs correctness as a result of testing).
- grumpyprole 4y ago
  > Given empirical studies, the current working hypothesis should be that if static types do have a positive effect on correctness, it is a small one. Which use cases, languages and static type systems are you referring to? The context is very important, especially when seeking to draw general conclusions from empirical studies. As someone who has previously posted extolling the merits of static analysis, I'm very surprised at your position regrding static types. Static types help to constrain a language and enable reasoning, either by additional static analysis or otherwise. It is precisely the flexibility of dynamic languages that makes them difficult to reason about and difficult to build correct software in. This is why the use of dynamic languages are mostly banned in the defense industry. Static types clearly help with composition (one of the complaints with Julia), especially at scale. How many academic empirical studies considered multimillion-line code bases? I submit for evidence a lot of expensive type-retrofitting projects such as Facebook Hack, Microsoft Typescript or Python types, which demonstrate that many companies have or had real problems with dynamic languages at any kind of scale.
- jolux 4y ago
  > 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 of structured programming and avoiding GOTO ever empirically proven, or did we all just collectively realize it was a good idea?
  - pron 4y ago
    > People get along fine without this feature, therefore there’s no sense in implementing it. As someone whose job is to add new features to a programming language, that's never been my argument. > But it cuts the other way, or we’d all still be using assembly High-level languages were satisfactorily shown to be more productive than Assembly. I don't claim that no innovation works, just that not all do, and certainly not to the same degree. That feature X is helpful is certainly no evidence that feature Y is helpful, and that Python is more productive than Assembly does not support the claim that programs in OCaml are more correct than programs in Clojure. Also, my argument isn't "we got by without it" or that no idea could ever work. It's that a specific claim was tested and unconfirmed. > Was the superiority of structured programming and avoiding GOTO ever empirically proven, or did we all just collectively realize it was a good idea? I don't know about the former, but the latter is certainly true, and until we actually reach concensus you can't claim we have. BTW, I certainly don't claim that types aren't useful or even that they're not better in some ways (I believe that they help a lot with tooling and organisation), but the particular claim that they universally help with correctness, and do so better than other approaches, was studied, and simply not confirmed. You can't come up with a claim, try and fail to support it time and again, and keep asserting it as if it's obviously true, despite the evidence.
    - jolux 4y ago
      > As someone whose job is to add new features to a programming language, that's never been my argument. 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. Forgive me for assuming this followed from that. > You can't come up with a claim, try and fail to support it time and again, and keep asserting it as if it's obviously true, despite the evidence. But “correctness” of itself is pretty nebulous. If we define it as whether or not the program conforms to one’s intentions with writing it, I would expect static types alone not to show a significant difference in correctness. Probably formal methods do but they have much higher overhead. However, in terms of eliminating patterns which are literally never correct, like dereferencing null pointers, violating resource lifetimes, or calling methods that don’t exist, static typing can in fact eliminate those patterns. > the claim that programs in OCaml are more correct than programs in Clojure My full-time job is Elixir so I know full well the consequences of maintaining large codebases in dynamic languages. I would switch to OCaml in a heartbeat if it ran on the BEAM! I want to know that I am calling functions correctly within a node when the module can be resolved at compile time. This is a really basic thing to want, and not one that dynamic languages can offer. The qualitative difference is similar to that between structured and unstructured programming: I can actually do local reasoning about a function without having to check all the call sites or write a lot of defensive tests. This is an obvious advantage, and on some level I don’t really care if it contributes to formal correctness or not because it would make my job easier.
mattkrause 4y ago
I'm surprised at this critique, as I thought Julia's type system was often considered to be one of its strongest features.
guenthert 4y ago
Julia allows you to specify the type of a datum if you feel the need (not unlike Common Lisp). Is any of the bugs the author mentioned related to the type system?

pron 4y ago

> 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 could come at the expense of others. I.e., even if types were shown to significantly help with correctness, it does not follow that if you want correctness your best course would be to add types. Given empirical studies, the current working hypothesis should be that if static types do have a positive effect on correctness, it is a small one (if it were big, detecting it would have been easy). Note that Matlab, the workhorse of scientific computing for a few decades now, is even less typed than Julia. That's not to say that Julia doesn't suffer from too many correctness issues (I have no knowledge on the matter), but even if it does, there is little support for the claim that typing is the most effective solution.

StefanKarpinski 4y ago
In particular, not a single issue mentioned in this article would have been prevented by static type checking.
- grumpyprole 4y ago
  This is not true. For example, the issue regarding custom index ranges causing silent data corruption (6 examples) could be fixed with static types. Look how many of the other bug reports contain the phrase "does not check for" or refer to specific primitive types.
  - adgjlsfhk1 4y ago
    it is only fixed with static typing and no generics (i.e. C/Fortran). If you have a generic array supertype, a statically typed language would let you write exactly the same bug.
    - grumpyprole 4y ago
      If one has a different type or trait for unusual and normal range indices, then the signature for the procedure that assumes indexing from 1 can be written to disallow other starting indices.
  - DNF2 4y ago
    How would static types help with that? Whether your indexing range starts with zero or one or something else isn't necessarily encoded in the type domain. `1:length(A)` is just a range of `Int`s.
    - grumpyprole 4y ago
      Why not encode the starting offset into the type domain? Or at least distinguish between normal and unusual. Then the function signature can restrict to 1-offset arrays if that is what it assumes internally.
      - DNF2 4y ago
        That means disallowing indexing with integers, I presume? Since an integer can take the values 0 or 1 equally. And what about the other end of the array. Must every index be restricted by type to be located in the acceptable range?
      - markkitti 4y ago
        If the function signature said `Array` rather than `AbstractArray`, then this code would have been fine. `Array` indexing starts at `1`. ``` julia> function f(A::Array) println(A[1:length(A)]) end f (generic function with 1 method) julia> f([1,2,3,4]) [1, 2, 3, 4] julia> f(OffsetArray(1:10, -1)) ERROR: MethodError: no method matching f(::OffsetVector{Int64, UnitRange{Int64}}) ``` You could prevent this problem using Julia's type system. The `AbstractArray` might have been too broad. Based on the chronology of the code that might not have been apparent. See other threads for details. Another way would be to treat `firstindex` as a trait and dispatch on that. ``` julia> f(A::AbstractArray) = f(A, Val(firstindex(A))) f (generic function with 1 method) julia> f(A::AbstractArray, firstindex::Val{1}) = println(A[1:length(A)]) f (generic function with 2 methods) julia> f(A::AbstractArray, firstindex::Val{T}) where T = error("Indexing for array does not start at 1") f (generic function with 3 methods) julia> f(A::AbstractArray, firstindex::Val{0}) = println("So you like 0-based indexing?") f (generic function with 4 methods) julia> f([1,2,3,4]) [1, 2, 3, 4] julia> using OffsetArrays julia> f(OffsetArray(1:10, 1)) ERROR: Indexing for array does not start at 1 Stacktrace: [1] error(s::String) @ Base .\error.jl:33 [2] f(A::OffsetVector{Int64, UnitRange{Int64}}, #unused#::Val{2}) @ Main .\REPL[5]:1 [3] f(A::OffsetVector{Int64, UnitRange{Int64}}) @ Main .\REPL[3]:1 [4] top-level scope @ REPL[9]:1 julia> f(OffsetArray(1:10, -1)) So you like 0-based indexing? ```
ThenAsNow 4y ago
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 typing/interface system Julia currently employs is at strong odds with compile-time correctness. There's almost certainly some middle ground to be discovered which might be unsound in a strict sense but pragmatically constrains code statically so there is high likelihood of having to go out of your way to pull the footgun trigger. You can see how little type annotations are used in practice in major Julia libraries. It should be integral to best practice in the language to specify some traits/constraints that arguments must satisfy to be semantically valid, but what you often see instead is a (potentially inscrutable) runtime error.
- pron 4y ago
  "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.
  - ThenAsNow 4y ago
    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 by the interpreter/compiler, how much time is spent on writing the implementation vs. writing & running tests, how many bugs occur on major refactorings, etc. If you have citations for studies you like, I'm certainly interested. My use of colloquialism aside, it is strictly more rigorous to catch equivalent bugs through the interpreter/compiler than through testing or other runtime-dependent approaches. In my own experience, despite being a more experienced programmer in my Julia-writing phase than in my OCaml-writing phase, it takes much more time to surface bugs in my "running" Julia code than OCaml. The lack of determinism in surfacing these bugs does not suggest as much confidence in the Julia code. You could counter by saying I'm probably able to implement more functionality in Julia per unit of up-front development time than the equivalent development time in OCaml, which I'd probably have to concede, but that just highlights measuring these things in a directly-comparable way is not easy. In the physical engineering disciplines, we often have disagreements about the level of sophistication of physics-based models that should be used for design and analysis. It's very reminiscent of these static vs. dynamic typing discussions in software development. There isn't a "one size fits all" answer, but generally, the more complex and expensive the system, the more important the models incorporate greater physical fidelity. My analogous conclusion here is a lot of technical/numerical code is complex enough that more rigor enforced by the language would likely be the right tradeoff for a net win on up-front correctness (vs correctness as a result of testing).
grumpyprole 4y ago
> Given empirical studies, the current working hypothesis should be that if static types do have a positive effect on correctness, it is a small one. Which use cases, languages and static type systems are you referring to? The context is very important, especially when seeking to draw general conclusions from empirical studies. As someone who has previously posted extolling the merits of static analysis, I'm very surprised at your position regrding static types. Static types help to constrain a language and enable reasoning, either by additional static analysis or otherwise. It is precisely the flexibility of dynamic languages that makes them difficult to reason about and difficult to build correct software in. This is why the use of dynamic languages are mostly banned in the defense industry. Static types clearly help with composition (one of the complaints with Julia), especially at scale. How many academic empirical studies considered multimillion-line code bases? I submit for evidence a lot of expensive type-retrofitting projects such as Facebook Hack, Microsoft Typescript or Python types, which demonstrate that many companies have or had real problems with dynamic languages at any kind of scale.
jolux 4y ago
> 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 of structured programming and avoiding GOTO ever empirically proven, or did we all just collectively realize it was a good idea?
- pron 4y ago
  > People get along fine without this feature, therefore there’s no sense in implementing it. As someone whose job is to add new features to a programming language, that's never been my argument. > But it cuts the other way, or we’d all still be using assembly High-level languages were satisfactorily shown to be more productive than Assembly. I don't claim that no innovation works, just that not all do, and certainly not to the same degree. That feature X is helpful is certainly no evidence that feature Y is helpful, and that Python is more productive than Assembly does not support the claim that programs in OCaml are more correct than programs in Clojure. Also, my argument isn't "we got by without it" or that no idea could ever work. It's that a specific claim was tested and unconfirmed. > Was the superiority of structured programming and avoiding GOTO ever empirically proven, or did we all just collectively realize it was a good idea? I don't know about the former, but the latter is certainly true, and until we actually reach concensus you can't claim we have. BTW, I certainly don't claim that types aren't useful or even that they're not better in some ways (I believe that they help a lot with tooling and organisation), but the particular claim that they universally help with correctness, and do so better than other approaches, was studied, and simply not confirmed. You can't come up with a claim, try and fail to support it time and again, and keep asserting it as if it's obviously true, despite the evidence.
  - jolux 4y ago
    > As someone whose job is to add new features to a programming language, that's never been my argument. 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. Forgive me for assuming this followed from that. > You can't come up with a claim, try and fail to support it time and again, and keep asserting it as if it's obviously true, despite the evidence. But “correctness” of itself is pretty nebulous. If we define it as whether or not the program conforms to one’s intentions with writing it, I would expect static types alone not to show a significant difference in correctness. Probably formal methods do but they have much higher overhead. However, in terms of eliminating patterns which are literally never correct, like dereferencing null pointers, violating resource lifetimes, or calling methods that don’t exist, static typing can in fact eliminate those patterns. > the claim that programs in OCaml are more correct than programs in Clojure My full-time job is Elixir so I know full well the consequences of maintaining large codebases in dynamic languages. I would switch to OCaml in a heartbeat if it ran on the BEAM! I want to know that I am calling functions correctly within a node when the module can be resolved at compile time. This is a really basic thing to want, and not one that dynamic languages can offer. The qualitative difference is similar to that between structured and unstructured programming: I can actually do local reasoning about a function without having to check all the call sites or write a lot of defensive tests. This is an obvious advantage, and on some level I don’t really care if it contributes to formal correctness or not because it would make my job easier.

mattkrause 4y ago

I'm surprised at this critique, as I thought Julia's type system was often considered to be one of its strongest features.

guenthert 4y ago

Julia allows you to specify the type of a datum if you feel the need (not unlike Common Lisp). Is any of the bugs the author mentioned related to the type system?