3 ms·

> 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 generaliza

> 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?

pjc50 5y ago
> 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 https://daringfireball.net/linked/2020/05/02/psychic-paper

pjc50 5y ago

> 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 https://daringfireball.net/linked/2020/05/02/psychic-paper