I think model theory is a really good source of theory to ground the notion of modules.
The relation between an interface and an implementation to me is very much the same as between a formal theory and a model of that theory.
I agree that in practice you'd want to use heuristics for this, but I think the benefits would be similar to learning a little bit of formal verification like TLA+, it's easier to shoot from your hip if you've studied how to translate some simpler requirements into something precise.
For a book like this you'd probably not need more than first order logic and set theory to get a sense of how to express certain things precisely, but I think making _reference to_ existing mathematics as what grounds our heuristics would've been beneficial.
Comments
I think model theory is a really good source of theory to ground the notion of modules.
The relation between an interface and an implementation to me is very much the same as between a formal theory and a model of that theory.
I agree that in practice you'd want to use heuristics for this, but I think the benefits would be similar to learning a little bit of formal verification like TLA+, it's easier to shoot from your hip if you've studied how to translate some simpler requirements into something precise.
For a book like this you'd probably not need more than first order logic and set theory to get a sense of how to express certain things precisely, but I think making _reference to_ existing mathematics as what grounds our heuristics would've been beneficial.