[dcow]

You need to learn some history. Or at least cite your claims.

We use type systems to help abstract patterns of data into logical constructs that can be reasoned about. They are logic systems with grammar that describes relationships between axioms and constructs.

Seriously, go read a textbook and then we can pick this discussion up. Wikipedia has a good overview.

https://en.m.wikipedia.org/wiki/Type_theory

[alxmng]

Ah, yes. Type theory originates before programming. Type theory only has relevance to computers insofar as it’s used to prove things about programs. Type theory in the context of computing is about programming.

We don’t call set theory and category theory “computer science” unless it’s about programming computers.

[joshuamorton]

No, I mean that's an application yes, but I'd still call Alonzo Church a computer scientist and his work theoretical computer science.

Much as how people who study computability are computer scientist, even though none of the asymptomatic improvements to matrix multiplication since 1990 are even remotely relevant to any kind of real-life program.