dimensional analysis is one of the great intellectual loves of my life; when I was in school it sometimes simplified things so much that it felt like I was cheating. later, as a professional computer scientist, the parallels with type-checking became obvious and super fun. anyhow this old Terrence Tao piece goes into the formal underpinnings of dimensional analysis -- luckily we don't need to care about this stuff to use it in practice! https://terrytao.wordpress.com/2012/12/29/a-mathematical-formalisation-of-dimensional-analysis/