It's a foundation of mathematics whose native objects are structures fundamental to higher mathematics (∞-groupoids, which are more or less equivalent to topological spaces up to homotopy), rather than awkward encodings (ZFC "sets", which are tree-like things), and where everything is automatically invariant with respect to abstract notions of equivalence (think isomorphism vs. equality).
The point is that it makes it much more realistic to check complicated math using computers, which will become more important as math inevitably gets more complicated.
Oh, and it happens to be a functional programming language. Which says something about functional programming.
The point is that it makes it much more realistic to check complicated math using computers, which will become more important as math inevitably gets more complicated.
Oh, and it happens to be a functional programming language. Which says something about functional programming.