A consistent thread running through the three decades of Voevodsky's work is
the application of the ideas of homotopy theory in new and surprising ways,
first to motives, and then to formalization of proofs and the foundations of
mathematics.  I will present the story of the latter development, focusing on
the points of interest to mathematicians.