5 ms·

After hearing "but Typescript is unsound!" a billion times.... kinda glad to se that being unsound is the "state of the art". I do wonder how far you can go wi

by rtpg 6y ago

After hearing "but Typescript is unsound!" a billion times.... kinda glad to se that being unsound is the "state of the art". I do wonder how far you can go without letting go of unsound-ness in practice though. Convenience is nice, guarantees are very very nice

gpm 6y ago
I don't see how this article supports the idea that "unsoundness" is state of the art?
- elmo2you 6y ago
  It may depend on age, overall knowledge of CS (including its history) and level of experience with multiple programming languages. Maybe the article itself does not literally support the idea, but it might still be inferred from it. It might also be the resulting discussion and responses, or additional field experience, that might give rise to this conclusion. I personally think the whole typing movement of the last decade has been mostly a red herring. What I mean with that is that it appears to try solve the "wrong" problem. While strong typing certainly can solve a whole class of bugs, my impression is that where this has been required most, ended up always situations where horrible overall design and code quality were the actual main problems (not typing). Coming from a (embedded) assembly and C direction myself, I have nothing against strong typing. But what has consistently rubbed me the wrong way about this modern strong typing "movement", both intuitively and rationally, is how it appears to fix something that is essentially broken on a whole different level. No amount of strong typing is going to fix that. I know, nothing much actionable or concrete here. Just my opinion. Regardless, this old geezer certainly agrees with the overall impression that "unsound" is pretty much the state of this art, these days.
  - bitwize 6y ago
    Static typing takes the burden of verifying certain forms of program correctness off the programmer and puts it in the compiler where it belongs, thus expanding the space of correct code the same programmer can write per unit cognitive load. The more kinds of things you check for in the type system (static lifetimes in Rust, for instance), the more benefits you get. It doesn't serve as a substitute for good taste, because while a mediocre programmer's reach is extended, a great programmer's reach is even further extended. Mediocre programmers can thus meaningfully contribute to embedded and kernel-level code under the tutelage of a good programmer without risking blowing the whole thing up, and increase their skill.
    - elmo2you 6y ago
      I get you point(s) and I guess you mean well. Statically typed languages do essentially what you said. They mostly (if not only) move data validation from run time to compile time. In dynamically typed languages, this often doesn't happen in the first place, while with static typing you are pretty much forced to. I have a little over 30 years of programming experience, the majority of it in statically typed languages (and quite a few). I have absolutely nothing against them (on the contrary). I still remember the rise in popularity of dynamically types languages, and how/why they were promoted. Faster development and code simplification, by only doing data validation where it was really needed (at run time), among them. Whether that was a good development, depends on where you stand. Do you care about correct software? Are you a business making software for profit, minimizing development costs? Are you part of a constantly growing market, where programmers who properly understand CS fundamentals are increasingly harder to find (or just more expensive)? Either way, to me it's no surprise that dynamically typed languages became as popular as they did, nor would I say that it is totally without merit (depending on your perspective). Sadly, it's also a heck of a lot easier to make utter garbage with dynamically typed languages. Not in the least because a programmer would no longer be confronted with their intellectual excrement at compile time. Unless all edge cases are properly tested during dev time, those usually become "user problems" during run time. People like me have frequently warned consultancy clients about the dangers of technologies and languages based on dynamically typed data, but more often than not other factors that were deemed more important. Fair enough, at least from a business perspective. Maybe not so much from an ethic and/or legal liability standpoint, but somehow the software industry has managed to create itself a rather unique immunity from legal consequence as the result of horrendous software quality (so good luck selling a need for better software). Sure, the contemporary static typing movement (as I like to call it) does appear to have genuine intentions to assist programmer (some of which should probably not even be allowed to code) to write substantially less buggy code. But I certainly do not agree with this idea that static typing will extend both mediocre and great programmers. In fact, if any of contemporary statically typed languages (or worse: ad-hoc extensions to dynamically typed languages) make somebody write substantially better software, then I firmly believe that this person either has fundamental CS related problems, or is being rushed/pressured too much to ever produce anything of considerable quality. I sincerely doubt that a statically typed language (or language add-on) will ever fix either of those. Such programmers will nonetheless still be good enough for a lot of regular programming gigs though. But, for the love of the gods, please keep those people miles away from anything embedded or kernel-level code. Again, I think you mean nothing but good. You may even know far more on the subject than I can expect, just based on your response. Either way, I certainly don't mean to offend you. Still, whenever I read a response like your's, I can't escape the feeling that it sounds more like a repeated mantra than that in comes from a deep understanding of the actual problem, including its long/complicated history.
fluffy87 6y ago
The state of the art is Idris, which has a sound, decidable, and extremely powerful type system. Most state of the art mainstream languages like Rust have sound but undecidable type systems. Many older languages with ad-hoc type systems are unsound, but there are also some older relatively used languages with powerful and sound type systems like Haskell.

by rtpg 6y ago

gpm 6y ago

I don't see how this article supports the idea that "unsoundness" is state of the art?

elmo2you 6y ago
It may depend on age, overall knowledge of CS (including its history) and level of experience with multiple programming languages. Maybe the article itself does not literally support the idea, but it might still be inferred from it. It might also be the resulting discussion and responses, or additional field experience, that might give rise to this conclusion. I personally think the whole typing movement of the last decade has been mostly a red herring. What I mean with that is that it appears to try solve the "wrong" problem. While strong typing certainly can solve a whole class of bugs, my impression is that where this has been required most, ended up always situations where horrible overall design and code quality were the actual main problems (not typing). Coming from a (embedded) assembly and C direction myself, I have nothing against strong typing. But what has consistently rubbed me the wrong way about this modern strong typing "movement", both intuitively and rationally, is how it appears to fix something that is essentially broken on a whole different level. No amount of strong typing is going to fix that. I know, nothing much actionable or concrete here. Just my opinion. Regardless, this old geezer certainly agrees with the overall impression that "unsound" is pretty much the state of this art, these days.
- bitwize 6y ago
  Static typing takes the burden of verifying certain forms of program correctness off the programmer and puts it in the compiler where it belongs, thus expanding the space of correct code the same programmer can write per unit cognitive load. The more kinds of things you check for in the type system (static lifetimes in Rust, for instance), the more benefits you get. It doesn't serve as a substitute for good taste, because while a mediocre programmer's reach is extended, a great programmer's reach is even further extended. Mediocre programmers can thus meaningfully contribute to embedded and kernel-level code under the tutelage of a good programmer without risking blowing the whole thing up, and increase their skill.
  - elmo2you 6y ago
    I get you point(s) and I guess you mean well. Statically typed languages do essentially what you said. They mostly (if not only) move data validation from run time to compile time. In dynamically typed languages, this often doesn't happen in the first place, while with static typing you are pretty much forced to. I have a little over 30 years of programming experience, the majority of it in statically typed languages (and quite a few). I have absolutely nothing against them (on the contrary). I still remember the rise in popularity of dynamically types languages, and how/why they were promoted. Faster development and code simplification, by only doing data validation where it was really needed (at run time), among them. Whether that was a good development, depends on where you stand. Do you care about correct software? Are you a business making software for profit, minimizing development costs? Are you part of a constantly growing market, where programmers who properly understand CS fundamentals are increasingly harder to find (or just more expensive)? Either way, to me it's no surprise that dynamically typed languages became as popular as they did, nor would I say that it is totally without merit (depending on your perspective). Sadly, it's also a heck of a lot easier to make utter garbage with dynamically typed languages. Not in the least because a programmer would no longer be confronted with their intellectual excrement at compile time. Unless all edge cases are properly tested during dev time, those usually become "user problems" during run time. People like me have frequently warned consultancy clients about the dangers of technologies and languages based on dynamically typed data, but more often than not other factors that were deemed more important. Fair enough, at least from a business perspective. Maybe not so much from an ethic and/or legal liability standpoint, but somehow the software industry has managed to create itself a rather unique immunity from legal consequence as the result of horrendous software quality (so good luck selling a need for better software). Sure, the contemporary static typing movement (as I like to call it) does appear to have genuine intentions to assist programmer (some of which should probably not even be allowed to code) to write substantially less buggy code. But I certainly do not agree with this idea that static typing will extend both mediocre and great programmers. In fact, if any of contemporary statically typed languages (or worse: ad-hoc extensions to dynamically typed languages) make somebody write substantially better software, then I firmly believe that this person either has fundamental CS related problems, or is being rushed/pressured too much to ever produce anything of considerable quality. I sincerely doubt that a statically typed language (or language add-on) will ever fix either of those. Such programmers will nonetheless still be good enough for a lot of regular programming gigs though. But, for the love of the gods, please keep those people miles away from anything embedded or kernel-level code. Again, I think you mean nothing but good. You may even know far more on the subject than I can expect, just based on your response. Either way, I certainly don't mean to offend you. Still, whenever I read a response like your's, I can't escape the feeling that it sounds more like a repeated mantra than that in comes from a deep understanding of the actual problem, including its long/complicated history.

fluffy87 6y ago

The state of the art is Idris, which has a sound, decidable, and extremely powerful type system. Most state of the art mainstream languages like Rust have sound but undecidable type systems. Many older languages with ad-hoc type systems are unsound, but there are also some older relatively used languages with powerful and sound type systems like Haskell.