It depends how you define CS; some people I work with don&#x27;t consider CS and Maths to be different subjects ;)<p>Personally, I find the topological perspective useful for thinking about types. I would guess most programmers think of types as sets, which is perfectly fine for the kind of first-order tasks we encounter in almost all day-to-day programming. However, it doesn&#x27;t give much intuition when dealing with the crazy kinds of abstractions we find in languages like Coq, Agda, or even some of the funky new Haskell extensions. Whilst the vast majority of programmers will never, and should never need to, deal with that level of abstraction, it&#x27;s personally the kind of programming I really enjoy :) (My own work is in the area of formal proofs, proof search, program equivalence, etc.)<p>I think HoTT&#x27;s key insight has already been made: although using UIP (or one of its many equivalents) to ignore the differences between proofs makes life easier in the short-term (eg. as a Coq user I was blown away by Agda&#x27;s ability to do pretty much everything by pattern-matching on refl), in the longer term all of those transport lemmas, path inductive proofs, etc. give us tangible benefits; firstly for explaining <i>why</i> something is true, secondly for allowing new kinds of higher-level reasoning and thirdly for aiding mechanisation and computation. Essentially, HoTT is just a logical extension of the intuitionism&#x2F;constructivism ideals :)<p>Hopefully HoTT, or something very much like it, will narrow the gap between what people know and what machines know.