[johncolanduoni]

Dependent types can help a lot when writing both of those actually. Idris' documentation contains an example interpreter that uses dependent typing (outside of theorem proving) heavily[1]. Compilers are a place where formal verification is likely worth it in some parts, particularly when writing optimization passes.

I think one of the biggest advantages of dependent typing is that it lets you implement a lot of things that other languages need to add as ad-hoc language features. A good example (if you're familiar with Haskell) is typeclasses. These can be done entirely at the value level in Idris, and IIRC interfaces are just syntactic sugar over this implementation. Other examples are generics that depend on values instead of types (without resorting to tedious things like type-level integers) and cleaner replacements for a lot of macro functionality.

[1]: http://docs.idris-lang.org/en/latest/tutorial/interp.html