Here's a bit of perspective. By "foundations" for mathematics, we mean a system of inference rules and axioms for mathematics. A very limited but correct view o

Here's a bit of perspective. By "foundations" for mathematics, we mean a system of inference rules and axioms for mathematics. A very limited but correct view of mathematics is that it is a game, where the inference rules are the available "moves", and the axioms are the "starting position". Given these two things, we can work out all the theorems we can possibly prove (this is because of Gödel's completeness theorem—not his incompleteness theorem, that's a different thing). Now, at this point a lot of programming-oriented people get confused, because they think, "how can you ever change the foundations? How can you do any math at all until you've completely formally defined the foundations of the subject?" This is a philosophical question, but in truth foundations of math aren't as hugely important as you might think. Here's an analogy: on both Windows and Linux you can write an email client. Now, the process will not be identical: some things that are easy on Windows are harder on Linux, and vice versa. But at the end of the day, the result on either platform will recognizable be an email client, and your major challenges will probably be email challenges, not platform challenges. Most mathematicians do not work at the foundations—they work at foundations for their specific field (a ring theorist cares about the properties of rings, not often the properties of sets, for example). You can analogize this to using a framework, like GTK for example. On the other hand, some subjects are poorly served by certain foundations, and some of the newer subjects in mathematics are running into that problem. The most pressing examples are category theory and homotopy theory, both of which are based on a study of operations, not objects, in a technical way that is poorly served by the current consensus foundation for mathematics. This would be like really wanting to write mobile apps—Windows would not be a good platform for it, and Android would be. As a PL theorist and kind-of-mathematician, I think the work going on in the Univalent Foundations project to be really interesting and extremely beautiful. I think it will have a profound impact on our understanding of mathematical foundations and higher-order logic, and I'm excited to see what comes of this effort. But I don't think it will really impact mathematics all that much—the impact of categorical thinking is the really important change, and that is helped, but not much, by new foundations.