🌶️ spicy take, software correctness
The common ways that software developers try to solve software correctness reminds me of broader societal issues...
Automated tests: don't try to solve the systemic problem, just institute enough procedures for specific cases and hope you've covered enough of it
Static type checking: don't try to solve the systemic problem, just treat everything and everybody as untrustworthy, you cannot trust anything that isn't verified by a computer
(Please do not reply with 'counterarguments' until you *really* understand where the analogies are coming from here)
re: 🌶️ spicy take, software correctness
@modulux I've elaborated a bit more here: https://social.pixie.town/@joepie91/110589790320844150
Additionally to that, I've never found the "making invalid states unrepresentable" argument to be a convincing one; I have yet to see a design that actually does so to a useful degree (ie. doesn't just specify memory types) while still remaining practically usable, and doing so in a way that's more efficient than other approaches.
re: 🌶️ spicy take, software correctness
@joepie91 Thanks for the clarification. I think I see what you mean, though I do find making invalid states unrepresentable possible and worthwhile. Especially using algebraic and dependent types. That said, I also see your point about it catching you once you made the error, but can't really think of how that could be avoided.
🌶️ spicy take, software correctness
@joepie91 I can see the analogy, but isn't making invalid states unrepresentable--which is a major object of static typing--dealing with a systemic problem?