5 ms·

For 20 years I’ve been writing entire applications in AWK, a dynamically typed language, and not once were any of the bugs due to typing. And yet, we’re such a

For 20 years I’ve been writing entire applications in AWK, a dynamically typed language, and not once were any of the bugs due to typing. And yet, we’re such a hopeless industry when most of us believe that a strongly typed system is essential for high quality software. It makes me despair even further about this profession.

naasking 9y ago
> For 20 years I’ve been writing entire applications in AWK, a dynamically typed language, and not once were any of the bugs due to typing. If you spent 20 years writing serious programs in Awk, I'm not convinced you know what real static typing is.
- Annatar 9y ago
  I had Ada as part of the core curriculum, just so we're clear. And being part of the cracking / demo scene, I grew up writing in MOS 6502 and MC68000 moving on to UltraSPARC assembler, so I just might know a thing or two about typing and what it actually translates to at the machine level. But, hey, barring suddenly landing a job working on SmartOS / illumos, that's also why I want to exit the computer industry: someone always isn't convinced and they think they know it better than I do. If I get out, anybody can not be convinced and know better for all I care at that point.
  - naasking 9y ago
    Machine level translation of language abstractions isn't relevant. Ada is an ok typed language, but still limited in many ways, but that's neither here nor there. The reason I can confidently state that you don't know what typing is, is because a type system is simply a means to prove propositions about your program. A type is a proposition. Any proposition, really. Most type systems employ propositions about simple equalities, inequalities and subsets, but there exist type systems that prove the absence of data races, deadlocks, the conformance to protocols, and even the time and space complexity of programs. So when you claim that none of your program bugs were a result of poor typing, you're literally claiming that none of these bugs resulted from treating a false proposition as if it were true. That's just nonsense. Literally every bug results from treating a false proposition as true. Even if we just stick with type systems dealing with simple equalities, like ML, claiming that none of your bugs would have been caught by types means that you never mistakenly considered two values as equal when they were not. Which is by itself exceedingly unbelievable. And even if you are that perfect, you clearly don't have a perfect understanding of your fellow, imperfect human beings who need tools to actually help them avoid mistakes.
    - Annatar 9y ago
      "Even if we just stick with type systems dealing with simple equalities, like ML, claiming that none of your bugs would have been caught by types means that you never mistakenly considered two values as equal when they were not." How could I mistake two values as equal when they were not? If I'm doing a cmp.b d0, #$31, either d0 will contain #$31 and it will be a byte or it won't. It can't be any other way (unless your central processing unit is designed by intel corporation)! In the line of work I do I don't normally design systems with locking, but I have designed them in the past and they worked fine by the way of empirical testing (purposely trying to cause a deadlock). I didn't need a formal system to prove it, nor would I ever trust such a system to ensure that my code or logic were correct. The rest is pure philosophy about provable code, and I've little appreciation for that: even Donald Knuth famously wrote beware of bugs in the above code; I have only proved it correct, not tried it. That's very instructive for one seeking insight, and I urge you to rethink your position on strong typing, because it's not the panacea you appear to believe it is. It doesn't make a difference if one is not a good programmer: in that case, nothing will save one. Not even being able to formally prove one's program logic is correct. Finally, I leave you with a theme from my childhood when I was learning to program: natural born coders I recommend meditating on it if you intend to continue working in the computer industry, because it's a real thing. They are few, but they do exist, and their work is unbelievable to behold. Even without them having used a strongly typed system to formally prove their code correct. https://www.youtube.com/watch?v=hvX6Y2bW4Z0 https://www.youtube.com/watch?v=hvX6Y2bW4Z0
      - naasking 9y ago
        > How could I mistake two values as equal when they were not? If I'm doing a cmp.b d0, #$31, either d0 will contain #$31 and it will be a byte or it won't. Testing equality with a constant is not the only equality test you make in programs. Firstly, what assurances do you even have that d0 actually is a byte? d0 could be a pointer so a byte comparison is invalid, unless you're doing some low-order bit pointer tagging. Secondly, comparisons where both operands are variables are where it starts getting murkier. > In the line of work I do I don't normally design systems with locking, but I have designed them in the past and they worked fine by the way of empirical testing (purposely trying to cause a deadlock). I didn't need a formal system to prove it, nor would I ever trust such a system to ensure that my code or logic were correct. You certainly need a formal system to prove it if you want to guarantee absence of deadlocks. You literally just said that you couldn't empirically trigger a deadlock, but that doesn't entail deadlocks don't exist. As for your distrust, I'm not interested in non-factual religious arguments. As for Knuth, you do realize he thinks that typical testing practices are often stupid, and that quote is him poking fun right? He informally proves most of the code he works with, and only does testing when he's still exploring an idea and he doesn't yet know what he wants. > It doesn't make a difference if one is not a good programmer: in that case, nothing will save one. Not even being able to formally prove one's program logic is correct. What kind absurdity is this? If you can prove your program's logic is correct, your program's logic is correct even if you're a bad programmer. It's a literal tautology. Finally, I have no idea why "natural born coders" has anything to do with what this thread is about. We're talking about what should be the standards and norms across a whole industry, not a select few who might not need them. Typing is not a panacea, but results are undeniably better with a decent, modern type system than without.

naasking 9y ago

> For 20 years I’ve been writing entire applications in AWK, a dynamically typed language, and not once were any of the bugs due to typing. If you spent 20 years writing serious programs in Awk, I'm not convinced you know what real static typing is.

Annatar 9y ago
I had Ada as part of the core curriculum, just so we're clear. And being part of the cracking / demo scene, I grew up writing in MOS 6502 and MC68000 moving on to UltraSPARC assembler, so I just might know a thing or two about typing and what it actually translates to at the machine level. But, hey, barring suddenly landing a job working on SmartOS / illumos, that's also why I want to exit the computer industry: someone always isn't convinced and they think they know it better than I do. If I get out, anybody can not be convinced and know better for all I care at that point.
- naasking 9y ago
  Machine level translation of language abstractions isn't relevant. Ada is an ok typed language, but still limited in many ways, but that's neither here nor there. The reason I can confidently state that you don't know what typing is, is because a type system is simply a means to prove propositions about your program. A type is a proposition. Any proposition, really. Most type systems employ propositions about simple equalities, inequalities and subsets, but there exist type systems that prove the absence of data races, deadlocks, the conformance to protocols, and even the time and space complexity of programs. So when you claim that none of your program bugs were a result of poor typing, you're literally claiming that none of these bugs resulted from treating a false proposition as if it were true. That's just nonsense. Literally every bug results from treating a false proposition as true. Even if we just stick with type systems dealing with simple equalities, like ML, claiming that none of your bugs would have been caught by types means that you never mistakenly considered two values as equal when they were not. Which is by itself exceedingly unbelievable. And even if you are that perfect, you clearly don't have a perfect understanding of your fellow, imperfect human beings who need tools to actually help them avoid mistakes.
  - Annatar 9y ago
    "Even if we just stick with type systems dealing with simple equalities, like ML, claiming that none of your bugs would have been caught by types means that you never mistakenly considered two values as equal when they were not." How could I mistake two values as equal when they were not? If I'm doing a cmp.b d0, #$31, either d0 will contain #$31 and it will be a byte or it won't. It can't be any other way (unless your central processing unit is designed by intel corporation)! In the line of work I do I don't normally design systems with locking, but I have designed them in the past and they worked fine by the way of empirical testing (purposely trying to cause a deadlock). I didn't need a formal system to prove it, nor would I ever trust such a system to ensure that my code or logic were correct. The rest is pure philosophy about provable code, and I've little appreciation for that: even Donald Knuth famously wrote beware of bugs in the above code; I have only proved it correct, not tried it. That's very instructive for one seeking insight, and I urge you to rethink your position on strong typing, because it's not the panacea you appear to believe it is. It doesn't make a difference if one is not a good programmer: in that case, nothing will save one. Not even being able to formally prove one's program logic is correct. Finally, I leave you with a theme from my childhood when I was learning to program: natural born coders I recommend meditating on it if you intend to continue working in the computer industry, because it's a real thing. They are few, but they do exist, and their work is unbelievable to behold. Even without them having used a strongly typed system to formally prove their code correct. https://www.youtube.com/watch?v=hvX6Y2bW4Z0 https://www.youtube.com/watch?v=hvX6Y2bW4Z0
    - naasking 9y ago
      > How could I mistake two values as equal when they were not? If I'm doing a cmp.b d0, #$31, either d0 will contain #$31 and it will be a byte or it won't. Testing equality with a constant is not the only equality test you make in programs. Firstly, what assurances do you even have that d0 actually is a byte? d0 could be a pointer so a byte comparison is invalid, unless you're doing some low-order bit pointer tagging. Secondly, comparisons where both operands are variables are where it starts getting murkier. > In the line of work I do I don't normally design systems with locking, but I have designed them in the past and they worked fine by the way of empirical testing (purposely trying to cause a deadlock). I didn't need a formal system to prove it, nor would I ever trust such a system to ensure that my code or logic were correct. You certainly need a formal system to prove it if you want to guarantee absence of deadlocks. You literally just said that you couldn't empirically trigger a deadlock, but that doesn't entail deadlocks don't exist. As for your distrust, I'm not interested in non-factual religious arguments. As for Knuth, you do realize he thinks that typical testing practices are often stupid, and that quote is him poking fun right? He informally proves most of the code he works with, and only does testing when he's still exploring an idea and he doesn't yet know what he wants. > It doesn't make a difference if one is not a good programmer: in that case, nothing will save one. Not even being able to formally prove one's program logic is correct. What kind absurdity is this? If you can prove your program's logic is correct, your program's logic is correct even if you're a bad programmer. It's a literal tautology. Finally, I have no idea why "natural born coders" has anything to do with what this thread is about. We're talking about what should be the standards and norms across a whole industry, not a select few who might not need them. Typing is not a panacea, but results are undeniably better with a decent, modern type system than without.