> related to mathematical theories like model theory, which give precise accounts of what it means to describe something
Perhaps too precise? APoSD is about the practical challenges of large groups of people creating and maintaining extensive written descriptions of logic. Mathematical formalisms may be able to capture some aspects of that, but I'm not sure they do so in a way that would lend real insight.
"How can I express a piece of complicated logic in an intuitive and easy-to-understand way" is fundamentally closer to writer's craft than mathematics. I don't think a book like this would ever be mathematically grounded, any more than a book about technical writing would be. Model theory would struggle to explain how to write a clear, legible paragraph.
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.