Oui, il est possible d'exprimer un type précis pour une routine de tri, de telle sorte que toute fonction ayant ce type doit en effet trier la liste d'entrée.
Bien qu'il puisse y avoir une solution plus avancée et élégante, je vais en esquisser une élémentaire, seulement.
f: nat -> nat0 .. 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) .
Un lemme simple peut facilement être prouvé.
Lemma lem1: forall n f, permutation n f -> m < n -> f m < n.
... (* from the def *)
mnhm < n
Definition nth {A} {n} (l: list A n) m (h : m < n): A :=
... (* recursion over n *)
Étant donné un ordre sur A, nous pouvons exprimer qu'une liste est triée:
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 :=
...
Enfin, voici le type d'un algorithme de tri:
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 *)
sn0 .. n - 1lsF( m ) < nnth
Notez cependant que c'est l'utilisateur, c'est-à-dire le programmeur, qui doit prouver que son algorithme de tri est correct. Le compilateur ne vérifiera pas simplement que le tri est correct: il ne fait que vérifier une preuve fournie. En effet, le compilateur ne peut pas faire beaucoup plus que cela: les propriétés sémantiques telles que "ce programme est un algorithme de tri" sont indécidables (par le théorème de Rice), nous ne pouvons donc pas espérer rendre l'étape de vérification entièrement automatique.
Dans un avenir très lointain, nous pouvons encore espérer que les prouveurs de théorèmes automatiques deviennent si intelligents que «la plupart» des algorithmes pratiquement utilisés peuvent être automatiquement prouvés comme corrects. Le théorème de Rice déclare seulement que cela ne peut pas être fait dans tous les cas. Tout ce que nous pouvons espérer, c'est un système correct, largement applicable, mais intrinsèquement incomplet.
Enfin, on oublie parfois que même les systèmes de type simples sont incomplets ! Par exemple, même en Java
int f(int x) {
if (x+2 != 2+x)
return "Houston, we have a problem!";
return 42;
}
est sûr de type sémantique (il retourne toujours un entier), mais le vérificateur de type se plaindra du retour inaccessible.
