Type theory is like this in particular. My background is mostly in classical math, and I was initially thrown off by the amount of symbols with special meaning

Type theory is like this in particular. My background is mostly in classical math, and I was initially thrown off by the amount of symbols with special meaning used in CS papers. An important realization was that most of the definitions behind these symbols (many I think borrowed from logicians) are actually quite straightforward, and the papers are not necessarily conceptually difficult so much as layered in their use of abstraction. I'll mention that Nederpelt and Geuvers' Type Theory and Formal Proof: An Introduction was recommended to me for this topic. I haven't had a chance to study it yet, but I'd say it's worth checking out.