Curry–Howard correspondence and functional programming "reliability"
The dependent types allow you to specify what properties your function should have, not just what its domain and codomain are. This way it becomes impossible to accidentally use the wrong function.
For example, suppose we want a function that sorts lists (of integers). In ordinary programming we would ask for a value of type List → List, and then we would write documentation in English that says &quot;and it is supposed to sort lists&quot;.
With dependent types, we would write down a fancier type:
Σ (f : List → List) Π (lst : List) isSorted(f lst) × isPermutation(lst, f lst)

(See below how one defines isSorted and isPermutation.)
An element of this type is a pair (f, p) such that f :  List → List and p is a function which takes as input any list lst and outputs a pair (q, r), such that: q is the proof that isSorted f lst and r is the proof that lst is a permutation of f lst. In other words, p proves that the output of f lst is precisely the sorted list lst.
If you think about it, it is impossible to accidentally use a non-sorting function. If you do, then you will not be able to also write down the proof that it really sorts lists.
In ordinary programming we are used to write down data and functions into the source code, but keep their properties in our heads. In dependent programming the properties are part of the source code, and so are the proof that those properties are satisfied.
P.S. We define isSorted : List → Type as
isSorted nil = True
isSorted (x :: lst) = (Π (y : int) . elementOf y lst → x ≤ y) × isSorted lst

It is a bit more annoying to define isPermutation, so I will not do it here.