Curry–Howard correspondence and functional programming "reliability"

The first time I heard about functional programming, someone told me "it's more reliable to code in a functional style because your type system is like a proof of correctness".

I recently learnt about the Curry-Howard (CH) correspondence and I think this is what he was using as a basis for his assertion about functional languages.

However, I have trouble understanding how far this leads to "more reliable programs".

Especially, here is my understanding:

• In the CH view, a function type A -> B is the same as an implication $A \implies B$ in some constructive view of logic, and so on... (union type, product of type, etc.)

• So if we end up being able to build an instance t of a type T it means we used only the available function types / implications using the available variables / assumptions.

Still, there are many ways a program written this way could be incorrect :

• If I have several variables a, b, c, ... of the same type A available, I may use a transformation A -> B on the wrong one.

• I may have different functions with the same signature A -> B but different use cases, and the type system won't be able to detect if I use the wrong one.

My questions are:

• In practice, do functional programming languages enforce things like "there should be no more than one instance of a type" or some variant to avoid those kinds of errors ?

• Is there a theoretical background in which we enforce more restrictions on functional languages and give the "more reliable" a stronger meaning ?

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 "and it is supposed to sort lists".

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.

StackExchange Computer Science Q#134518, answer score: 4