That's all true from the fact that there are real correspondences with math theories. But like, that's the whole point of applied math no? To find correspondences with other things so that we can then leverage and apply the math principles to that thing?
I'm sure there's quite many things in programming language where you can use such correspondence to your advantage, not just ADTs. But we don't teach it starting from the mathematical correspondence and then back.
To put it more simply, most programming isn't thought by first teaching learners about theoretical computer science. Generally it happens either in parallel or you learn the theory after the fact. But for some reason, when it comes to functional programming it seems most teachers want to start with teaching you the theory.
And my above point is that, even historically, it is not always true that theory came first. Often times, the construct were invented and used practically from finding solutions to concrete problems, and later a theory around it was developed. In the case of ADTs, I'm not 100% sure which came first, but I know they were first implemented in the programming language Hope. Not sure if the theory was there prior or not.