3 ms·

"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

"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.
- Annatar 9y ago
  “Firstly, what assurances do you even have that d0 actually is a byte?“ Because of .b in cmp.b; in assembler you control exactly what goes in and what goes out. If you are comparing bytes, then bytes it must be; the rest of the register is ignored. And if you’re cmp.l d0, #$31 comparing longwords, then you already know what you’re expecting and the very nature of the way that works is that it either works or doesn’t. cmp.b d0,d1, same deal. You’re trying to elevate something trivial (formal proof) to something more valuable and important than it really is. And one more thing: a bad programmer will never make an effort to formally prove the logic in his program or use a strongly typed system for that matter. And a good programmer? Well, considering that Rust is utter overcomplicated garbage mishmash, that pretty much only leaves Ada as the only realistic tool of choice, but Ada is also not a very good tool: one thing that remains seared in my mind was the acute lack of documentation on the language, especially on how to solve real world problems, which makes Ada impractical. Where does that leave us? It leaves us with our own brain, knowledge, experience and insight to not write crappy software. Sorry that you feel that strong typing is a valuable tool, but practice and reality disagree with you, as is often the case in life. Better concentrate on how to write high quality software without it, or else you won’t get too far, and what benefits you do claim aren’t worth it, no matter how well it sounds in theory. Is being able to formally prove one’s program logic better than not being able to do so? Of course. But the programming languages, the tools to do that, are utter overcomplicated garbage. You’d have an easier time and be more productive coding in assembler where you control everything, then using a piece of overcomplicated trash fire that is Rust, for example. The entire typing thing is really just a made up crutch necessitated by artificial abstractions by high level programming languages: when I look at the data you’re sending me from the high level language in my assembler code, it’s all bits, the only thing the hardware understands, the reality. So do yourself a favor, don’t make it more complex than it needs to be. Computers are already an overcomplicated pain in the ass, let’s not try to turn it into rocket science, because it can never be that.

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.

Annatar 9y ago
“Firstly, what assurances do you even have that d0 actually is a byte?“ Because of .b in cmp.b; in assembler you control exactly what goes in and what goes out. If you are comparing bytes, then bytes it must be; the rest of the register is ignored. And if you’re cmp.l d0, #$31 comparing longwords, then you already know what you’re expecting and the very nature of the way that works is that it either works or doesn’t. cmp.b d0,d1, same deal. You’re trying to elevate something trivial (formal proof) to something more valuable and important than it really is. And one more thing: a bad programmer will never make an effort to formally prove the logic in his program or use a strongly typed system for that matter. And a good programmer? Well, considering that Rust is utter overcomplicated garbage mishmash, that pretty much only leaves Ada as the only realistic tool of choice, but Ada is also not a very good tool: one thing that remains seared in my mind was the acute lack of documentation on the language, especially on how to solve real world problems, which makes Ada impractical. Where does that leave us? It leaves us with our own brain, knowledge, experience and insight to not write crappy software. Sorry that you feel that strong typing is a valuable tool, but practice and reality disagree with you, as is often the case in life. Better concentrate on how to write high quality software without it, or else you won’t get too far, and what benefits you do claim aren’t worth it, no matter how well it sounds in theory. Is being able to formally prove one’s program logic better than not being able to do so? Of course. But the programming languages, the tools to do that, are utter overcomplicated garbage. You’d have an easier time and be more productive coding in assembler where you control everything, then using a piece of overcomplicated trash fire that is Rust, for example. The entire typing thing is really just a made up crutch necessitated by artificial abstractions by high level programming languages: when I look at the data you’re sending me from the high level language in my assembler code, it’s all bits, the only thing the hardware understands, the reality. So do yourself a favor, don’t make it more complex than it needs to be. Computers are already an overcomplicated pain in the ass, let’s not try to turn it into rocket science, because it can never be that.