Dependent types provide an unprecedented level of type safety. A quick example is a type-safe printf implementation (video). They are also useful for theorem proving. According to the Curry-Howard correspondence, mathematical propositions can be represented in a program as types. An implementation that satisfies a given type serves as a proof of the corresponding proposition. In other words, inhabited types represent true propositions.
The Curry-Howard correspondence applies to every language with type checking. But the type systems in most languages are not expressive enough to build very interesting propositions. On the other hand, dependent types can express quantification (i.e., the mathematical concepts of universal quantification (∀) and existential quantification (∃)). This makes it possible to translate a lot of interesting math into machine-verified code.