HOTT (homotopy type theory) is logic built on type theory (mostly from Computer Science) and ideas from topology to give foundations of mathematics that are very elegant and much closer to mathematical practice. This makes HOTT very useful for computer proof systems, and also gives a very nice new synthetic treatment of homotopy theory.