[Solved]: Proving a sorting operation in type system

Definition permutation (n: nat) (f: nat -> nat): Prop :=   (* once restricted, its codomain is 0..n-1 *)   (forall m, m < n -> f m < n) /   (* it is injective, hence surjective *)   (forall m1 m2, m1 < n -> m2 < n -> f m1 = f m2 -> m1 = m2) . 

A simple lemma can easily be proved.

Lemma lem1: forall n f, permutation n f -> m < n -> f m < n. ... (* from the def *) 

We define what is the $m$th element of a list having length $n$. This function requires a proof h stating that $m<n$ indeed holds.

Definition nth {A} {n} (l: list A n) m (h : m < n): A := ... (* recursion over n *) 

Given an ordering on A, we can express that a list is sorted:

Definition ordering (A: Type) :=    { leq: A->A->bool |      (* axioms for ordering *)      (forall a, leq a a = true) /      (forall a b c, leq a b = true -> leq b c = true -> leq a c = true) /      (forall a b, leq a b = true -> leq b a = true -> a = b)     } .  Definition sorted {A} {n} (o: ordering A) (l: list A n): Prop := ... 

Finally here’s the type for a sorting algorithm:

Definition mysort (A: Type) (o: ordering A) (n: nat) (l: list A n):    {s: list A n | sorted o s /                   exists f (p: permutation n f),                   forall (m: nat) (h: m < n),                       nth l m h = nth s (f m) (lem1 n f p h) } := ... (* the sorting algorithm, and a certificate for its output *) 

The output type states that the result list s is $n$ elements long, it is sorted, and that there’s a permutation of $0..n-1$ that maps the elements in the input list l to the ones in the output list s. Note that we have to invoke the lemma above to prove $f(m) < n$, which is required by nth. Note however that it is the user, i.e. the programmer, which has to prove their sorting algorithm correct. The compiler will not simply verify that the sorting is correct: all it does is checking a provided proof. Indeed, the compiler can not do much more than that: semantic properties such as “this program is a sorting algorithm” are undecidable (by Rice theorem), so we can not hope to make the proving step fully automatic. In the far, far future, we can still hope that automatic theorem provers get so smart that “most” practically used algorithms can be automatically proved correct. The Rice theorem only states that this can not be done in all cases. All we can hope for is a correct, widely applicable, but inherently incomplete system. As a final note, it is sometimes forgotten that even simple type systems are incomplete! E.g. even in Java

int f(int x) {    if (x+2 != 2+x)       return "Houston, we have a problem!";    return 42; } 

is semantically type safe (it always returns an integer), but the type checker will complain about the unreachable return.