Voevodsky left us far too early :( I share his concerns completely and have started studying the Lean theorem prover as a practical means for verification; although the theoretical basis for Lean is the Calculus of Inductive Constructions which is, as I understand it, incompatible with the univalence axiom.
At the end of the day, using whichever foundations you prefer, I encourage young mathematicians to look into proof assistants, and interested computer scientists to develop them; the more independent verifiers we have, the better.
I am rather interested in this line of work for both mathematicians and computer scientists. What is the best way to get started? What's the quickest way to get up to speed in this field?
I am a cluebie in this field, but I guess working your way through some Lean tutorials [1], and/or reading the introduction to the HoTT book [1] might either scare you off, or get you enthused enough to continue.
I have never managed to understand why you need univalent foundations as opposed to just using some dependent type theory like Lean. As far as I see Lean could do all the mathematics I could imagine. I can only imagine that univalent foundations could help make things cleaner, but for now Lean seems good enough.
At the end of the day, using whichever foundations you prefer, I encourage young mathematicians to look into proof assistants, and interested computer scientists to develop them; the more independent verifiers we have, the better.