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.
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.
Look how many of the other bug reports contain the phrase "does not check for" or refer to specific primitive types.
``` 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? ```
But you will still want to calculate indices at runtime, and then out-of-bounds errors will have to be caught at runtime anyway.
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.
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).
Here's a good talk to watch on the subject: https://youtu.be/ePCpq0AMyVk
And here's a summary of various studies done: https://danluu.com/empirical-pl/
As of today, what we know is that if there's a positive effect of types on correctness, then it is probably a small one.
There's really no need to assert what is really a conjecture, let alone one that's been examined and has not been verified. 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 okay to prefer typed languages even though they do not, as far as we know, have a big impact on correctness.
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.
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."
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.
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.
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.
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.
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.
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.
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.
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.
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.
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?
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.
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.
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 correct, like dereferencing null pointers, violating resource lifetimes, or calling methods that don’t exist, static typing can in fact eliminate those patterns.
But the implication is reveresed! From A => B, i.e. types prevent certain bad things, you're concluding B => A, i.e. if you don't want those bad things then you should use types. That simply does not follow.
> 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.
I wouldn't dare imply that types don't have certain important advantages, but that doesn't support the specific claim that types generally and significantly improve correctness — which many have tried to show and failed — and it certainly doesn't support the much stronger claim that if you want to improve correctness, the most effective way to do it is to use types.
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 prevent certain bad things, you're concluding B => A, i.e. if you don't want those bad things then you should use types. That simply does not follow.
I really don’t know of a simpler way to do this than types. Do you? Honestly I would be using it if I did. All of the solutions I know to these problems involve types.
> that doesn't support the specific claim that types generally and significantly improve correctness — which many have tried to show and failed
What definition of correctness is being used here? Surely you’re not saying that optionals don’t eliminate null pointer dereferencing, are you?
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...
Right, but this is why I asked about structured programming. These things are hard to study by their nature. I understand there’s not a consensus on this, but there are a lot of programmers who feel quite strongly that static types reduce bugs. Maybe that’s not good enough for you! But it’s clear that you accept other practices as beneficial on insufficient evidence. Or maybe you don’t — maybe you don’t think writing correct unstructured programs is harder.
> most catastrophic crashes in distributed systems occur not because programmers fail to consider certain exceptional situations
This is irrelevant though. The question is not whether static types prevent the most common types of bugs, or the most dangerous (it’s clear that memory safety is more important than static types in that regard.) If static types narrow the problem space to situations where you explicitly made the wrong decision, that’s significant. If there are any bugs caused by not handling exceptional conditions (and we both know that there are), then static type systems help reduce those.
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 beneficial on insufficient evidence
It's not about "accept." I myself practice typed programming without asserting the empirical claim that it reduces bugs, that seems not to be true (or at least, the effect does not seem to be big).
> The question is not whether static types prevent the most common types of bugs, or the most dangerous
So far, we've failed to show that static types reduce bugs, period. You're allowed to like them and promote them, but your feeling towards them does not make a specific empirical claim more or less true.
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 about type systems than random people do about homeopathy.
> or at least, the effect does not seem to be big
Fair enough! It’s probably not as big as testing or code review but I do think it exists. You mentioned the TypeScript study, it’s not like there’s no evidence for believing this like there is with homeopathy.
> So far, we've failed to show that static types reduce bugs, period.
I mean, how could they not? You still haven’t explained this part, except with vague allusions that the problems they catch are not the most common problems. I’ve explained how static types reduce bugs: by eliminating cases where you intend to handle a case and forget to. I’ll specify that I mean a type system with exhaustivity checking or narrowing with control flow (like TS or Kotlin). This is not an empirical argument, it’s a rational argument, and I still legitimately don’t understand what the flaw is. The way I see it, static type systems restrict operations on types to those known to be valid at compile time. In a sound type system and compiler, the resulting program is guaranteed not to make invalid operations on types at runtime. Dynamic programs are fully free to make invalid operations on types at runtime. Some number of bugs are caused by making invalid operations on types at runtime. Where are those bugs in a statically typed program, if they haven’t been eliminated?
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.
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.
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.
> 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.
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.
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.
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.
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."
But that doesn't mean they have fewer bugs! They might well have more.
> What I'm saying is that the set of possible incorrect runtime behaviors is smaller in a static language.
Not exactly. For every program in an untyped language, you could write a typed program with the exact same behaviours.
The assertion that typed programs have fewer bugs is simply false in theory, and failed to be confirmed empirically.
> 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."
I understand that that is your belief, but it is supported by neither theory nor practice.
“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 the evidence base around types, and I agree with your conclusions; my beef here is just with divorcing the language of formal logic from its substance.
not very many in my experience - matlab rots the brain