The seeds of homotopy type theory

I was recently very surprised to find a lecture (http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf) of Vladimir Voevodsky explaining his motivation for working on homotopy type theory and the mechanization of mathematics.

In brief the reason was that a group of well-known mathematicians working on "higher dimensional mathematics" since the 1980's were making errors which were not discovered for years, in one case not till more than 20 years after publication. Voevodsky refers to this situation as "outrageous".



He concludes that "mathematics is in need of a completely new foundation" and in particular that the categorical foundations for mathematics are inadequate for its formalization.

He is satisfied with Univalent Foundations and the proof assistant Coq.

His key statement is that: "I now do my mathematics with a proof assistant and do not have to worry all the time about mistakes in my arguments or about how to convince others that my arguments are correct."

I firmly disagree with the need to mechanize mathematics (though not with the usefulness of computer calculation).
In my view mathematicians are obliged to "convince others" by normal human discourse, however difficult and sometimes imperfect that process may sometimes be.