When I studied mathematics in college, I really loved algebraic topology, set theory and (first-order) logic. After a graduate course in computer science, I was fascinated by automated theorem proving, constructive proof and type theory. The foundations of mathematics has also been a subject that has interested me.
I came across the Homotopy Type Theory site a few weeks ago while following a link from this blog post where the author discusses the meaning of proof in mathematics. HTT is an attempt to re-launch the foundations of mathematics on a more constructive computational footing. A book written as part of a year long special program at the IAS is available here with an introductory chapter that gives a very good overview of Type Theory.
One of the interesting parts of Type Theory, that can be instantly related to computer science applications is the notion of dependent types. This paper shows some of the uses of this concept.
There team are working hard to get many of their proofs verified by proof assistants such as COQ, so perhaps we really entering a new age of mathematics.