I think you misunderstand what "correctness" is really about. To me at least it's about creating a small set of powerful abstractions that can be applied generally to any problem. In order for those abstractions not to "leak" they need be really rigorously defined. The alternative I think is to have a lot of ad-hoc abstractions for each application that break as soon as requirements change. I really, really disagree with the idea that bad code that ships is always better than code that doesn't. That is how we get software that is riddled with security issues. Even if the specific application isn't that important, it very well might be a major catastrophe if it has a severe security vulnerabilities that allows an attacker to get a root shell on a server in your internal network.
> I really, really disagree with the idea that bad code that ships is always better than code that doesn't. That is how we get software that is riddled with security issues. Even if the specific application isn't that important, it very well might be a major catastrophe if it has a severe security vulnerabilities that allows an attacker to get a root shell on a server in your internal network.
Your argument fails to be an argument at all.
Can you justify that first sentence? I do not see any convincing reason why you disagree... or even any reasons here tbh.
I assume by first sentence you mean the statement that "That is how we get software that is riddled with security issues"
The argument is that you assume that the minimum value of code is zero, so that any code that ships has to be better than code that doesn't ship because at worst it is worthless, which is the same value as code that doesn't ship.
My point is that bad code can be worth less than zero if it actively causes harm. So for example, code that has a critical security vulnerability which leaks personal information is worse than nothing. You would be better off not shipping anything at all than shipping something that causes actual harm.
