5 ms·

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

• 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.
    • pron 4y ago
      > 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 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.
      • jolux 4y ago
        > 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 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?
        • 4y ago
• nancarrow 4y ago
  > How many Matlab users know things could be better? not very many in my experience - matlab rots the brain