The Univalent Foundations of Mathematics is a new foundational system, proposed by Vladimir Voevodsky, building on a recently discovered deep connection between logic (more precisely, type theory) and homotopy theory. Many logical methods can be then applied to problems from homotopy theory and, conversely, homotopy-theoretic viewpoint is useful in understanding some logical constructions. In the talk, I will explain this connection and survey the main results of the Univalent Foundations program.