“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

“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.