Comment by pron
2 days ago
Soundness means that the program behaves in accordance with what its types express. You're right that C may be unsound due to undefined behaviour, but I don't think this is about soundness. What you're saying is that papers on types show how you can use types to express more constraints.
There can be other valid perspectives and definitions of that word than yours.
I think almost all (tech) arguments stem from simple disagreements and/or different assumptions made on the definition of a (subjective) term.
You may be right in general, but soundness comes from formal logic, where they're pretty fastidious with their definitions. Soundness certainly doesn't mean the expressivity of the types (i.e. what constraints they can represent); it's about the relationship between the runtime behaviour of a program and the types in the code.
Again I think you're trying to push a specific definition as more correct than OP's somehow. Why not just ask them what they meant to understand their intent/context instead of saying they are wrong?
Unless the point of your argument isn't to understand OP but simply to "win."
1 reply →