Types guarantee properties over the full set of possible inputs before you run any code. If you can enforce a property with a type, it is IME far less work than trying to enforce that property with a test.
"Less strict" inevitably means not caring about a bunch of edge cases. It's a bit like "overflow is undefined behavior in C"; nobody wants to care about how "i++" is a statement that's (a) absolutely everywhere and (b) potentially invokes undefined behavior at runtime, so the only way to guarantee that out involves a lot more proof work somewhere.
If you can enforce a property with a type, it is IME far less work than trying to enforce that property with a test.
That's an unnecessarily broad generalization to a concrete statement, and if it were true more people would write their programs in dependently typed programming languages or whatever.
nobody wants to care about how "i++" is a statement that's (a) absolutely everywhere and (b) potentially invokes undefined behavior at runtime, so the only way to guarantee that out involves a lot more proof work somewhere.
In many domains, the high standards you're displaying here will almost immediately throw you out of business.
In particular "i++" for most applications is just fine to write without any second thoughts. It's not even a good idea to write a test. Just run the program and fix it in the rare case something it doesn't work as expected (it's almost a safe bet the issue won't UB).
You're not taking a tank to go to the supermarket either, are you?
more people would write their programs in dependently typed programming languages or whatever.
Programming language choice is greatly influenced by ecosystem factors. If you wanted to write a program for the browser, you had to write it in Javascript - so people went to considerable lengths to fit typed front ends onto Javascript.
Just run the program and fix it in the rare case something it doesn't work as expected (it's almost a safe bet the issue won't UB).
You're not taking a tank to go to the supermarket either, are you?
No, but if you're going into a live fire hostile environment you might want a tank, and the internet is such an environment. If there is a bug in your parser, and the parser is exposed to untrusted data, then that's a potential avenue for exploit.
Less of an issue in managed-runtime languages, but it's still possible to have semantic level exploits. I remember there was one for Apple which exploited the fact that there were different proplist parsers. https://daringfireball.net/linked/2020/05/02/psychic-paper
Comments
Types guarantee properties over the full set of possible inputs before you run any code. If you can enforce a property with a type, it is IME far less work than trying to enforce that property with a test.
"Less strict" inevitably means not caring about a bunch of edge cases. It's a bit like "overflow is undefined behavior in C"; nobody wants to care about how "i++" is a statement that's (a) absolutely everywhere and (b) potentially invokes undefined behavior at runtime, so the only way to guarantee that out involves a lot more proof work somewhere.
That's an unnecessarily broad generalization to a concrete statement, and if it were true more people would write their programs in dependently typed programming languages or whatever.
In many domains, the high standards you're displaying here will almost immediately throw you out of business. In particular "i++" for most applications is just fine to write without any second thoughts. It's not even a good idea to write a test. Just run the program and fix it in the rare case something it doesn't work as expected (it's almost a safe bet the issue won't UB).
You're not taking a tank to go to the supermarket either, are you?
Programming language choice is greatly influenced by ecosystem factors. If you wanted to write a program for the browser, you had to write it in Javascript - so people went to considerable lengths to fit typed front ends onto Javascript.
No, but if you're going into a live fire hostile environment you might want a tank, and the internet is such an environment. If there is a bug in your parser, and the parser is exposed to untrusted data, then that's a potential avenue for exploit.
Less of an issue in managed-runtime languages, but it's still possible to have semantic level exploits. I remember there was one for Apple which exploited the fact that there were different proplist parsers. https://daringfireball.net/linked/2020/05/02/psychic-paper