Dependent types are the reason why Idris can formally prove mathematical statements, compared to other programming languages.
Actually it's even cooler than this. Dependent types are not what make proofs possible. What's happening here is there's a deep correspondence between type systems and logical formalisms, the Curry-Howard-Lambek correspondence.
Simply typed lambda calculus corresponds to propositional logic with natural deduction (zeroth order).
Dependently typed lambda calculus corresponds to predicate logic with natural deduction (first order).
What makes dependent types cool is that they allow proofs of statements involving first-order predicates. I think this helps explain why they are so much more powerful than simple types - they are a step up in power (literally) analogous to the step from propositional logic to predicate logic.
Re. this footnote:
Actually it's even cooler than this. Dependent types are not what make proofs possible. What's happening here is there's a deep correspondence between type systems and logical formalisms, the Curry-Howard-Lambek correspondence.
Simply typed lambda calculus corresponds to propositional logic with natural deduction (zeroth order). Dependently typed lambda calculus corresponds to predicate logic with natural deduction (first order).
What makes dependent types cool is that they allow proofs of statements involving first-order predicates. I think this helps explain why they are so much more powerful than simple types - they are a step up in power (literally) analogous to the step from propositional logic to predicate logic.