Lambda the Ultimate

I have a question for which I expect a good answer from Matt M, Andreas Rossberg, or Jules Jacobs, should any of these folks feel inclined to reply, because they clearly know a lot about type systems.

Is type theory math? How is discussing type theory also discussion of programming language? When analyzing types in a specific PL, I can see type theory informing analysis of that PL. But when talking about type systems in the abstract, apart from a PL, it just sounds like philosophy of algebra to me. I can't find the PL angle unless the idea is that all programming languages should be about math. What I'm trying to do is put type theory discussion in context. What is it good for? (I hope asking a simple brass-tacks question is not rude.)

I don't mind getting beat up as long as it's educational. :-) But I'm trying to express curiosity rather than a challenging attitude. Edit: I'm going from my personal reaction to type theory discussions, rather than anything I read. I hope to learn something, rather than push my impression that type theory is just math. So a reasoned contradiction would be interesting.