[hootbootscoot]

Maybe I'm being terribly naive, but I don't see this from a maths perspective at all, I see this as about the shape of data and about memory allocation. If one increments pointers across an array of data, one should know the stepping size, for example.

How is this (programming/practical) side of the word "type systems" related to formal/mathematical "type systems"?

I missed that part

[Koshkin]

Types are a kind of constraints on what kind of logical constructs in one case, and what kinds of computational constructs in the other, are allowable. Logic and computation are related, but they are not the same. (This difference is also evident in how people think about monads in programming vs. how they are defined and used in category theory.)