It is great that someone with a Fields medal is interested in interactive theorem proving. And he is right that mathematics will completely change because of it. Soon.
I doubt though that HoTT is the way this revolutionary change will happen. If you don't believe me, try reading the first few pages of chapter 2 of the HoTT book. It is basically total gibberish to me, and yes, this is because I am neither well versed in constructive type theory, nor in homotopy theory. I DO have though 10+ years of experience in interactive theorem proving, as well have a diploma in math where I learnt the basic notions of topology. Now, if this is gibberish to me, it will be gibberish to about 99% of all mathematicians out there .
A revolution does not happen by excluding 99% of its targeted population. HoTT will have to evolve into something much easier to understand with a clear value proposition to non-homotopy / non-type-theorists before I would even remotely consider it for providing the underpinnings of a system for interactive proof.
I doubt though that HoTT is the way this revolutionary change will happen. If you don't believe me, try reading the first few pages of chapter 2 of the HoTT book. It is basically total gibberish to me, and yes, this is because I am neither well versed in constructive type theory, nor in homotopy theory. I DO have though 10+ years of experience in interactive theorem proving, as well have a diploma in math where I learnt the basic notions of topology. Now, if this is gibberish to me, it will be gibberish to about 99% of all mathematicians out there .
A revolution does not happen by excluding 99% of its targeted population. HoTT will have to evolve into something much easier to understand with a clear value proposition to non-homotopy / non-type-theorists before I would even remotely consider it for providing the underpinnings of a system for interactive proof.