Yes, it is possible to express a precise type for a sorting routine, such that any function having that type must indeed sort the input list.
While there might be a more advanced and elegant solution, I'll sketch an elementary one, only.
We will use a Coq-like notation. We start by defining a predicate requiring that f: nat -> nat acts as a permutation on $0..n-1$:
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.
