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.
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.