Dependent types?

Question

Programming

Hello. I seem to understand what dependent types are (using simple examples), there are even various articles on this topic on Habré.
However, can someone explain what is the benefit? Well, in general, explain what is happening. Any evidence, verification, what does it give? According to the link of that article, as I understand it, we have two things - a sorting algorithm (it is not known which one) and a proof that it (is it exactly?) Correct.
In general, please explain what dependent types are, how they work, and what the evidence has to do with it. Thank you.

Answer 1

I explain: mathematicians have noticed a connection between programs and mathematical proofs (here we read about the Curry-Howard isomorphism). So the predicate calculus corresponds to the lambda calculus with dependent types.
This is an explanation on the fingers.
Read more in Pierce's textbook Types in Programming Languages.