Dependent type theory, which enriches simple type systems with types that can explicitly refer to programs, is a foundation for both mathematics and programming. Dependent types are the basis of proof assistants such as Agda, Coq, Idris, Twelf, and NuPRL, and various forms of dependency are making their way into more mainstream languages such as Haskell and OCaml. Dependent type theory has applications to program verification, computer-checked mathematical proofs, programming language metatheory and compiler verification, generic programming, and many other areas of programming and programming languages research. Some research projects in dependent types are very mathematical, studying enrichments of the basic systems of dependent type theory – for example, to better integrate effectful programming, or to better describe some mathematical concept that is to be formalized. Other projects are more engineering, such as building a large verified software artifact or mathematical proof using existing proof assistants. In this talk, I will show some small examples of dependently types programming, to give you a taste for what it is and can do, and survey some of the current research directions in the field.