Re: Un peu déçu par Rust

J'ai regardé un peu la documentation de Idris et je ne suis pas convaincu que cela simplifie les choses par rapport à Coq.

Une des fonctionnalité centrale des langages avec types dépendants (les types sont des citoyens de première classe, comme les fonctions le sont dans les langages fonctionnels) est de pouvoir prouver des théorèmes de spécification et de correction sur les programmes. Or quand je lis les deux exemples de la documentation : l'addition est associative sur les entiers et l'addition est commutative, je ne trouve pas cela plus simple. Il faut écrire un module dans un fichier avec une preuve laissée indéterminée, chargé le module dans la REPL, utiliser les tactiques pour effectuer la preuve puis recopier le script de preuve dans le fichier.

Avec CoqIde, pour la preuve d'associativité j'écris cela dans un fichier :

(* je remets la définition du type nat et de la fonction plus *)
Inductive nat :=
 | O : nat
 | S : nat -> nat.
Fixpoint plus n m :=
 match n with
 | O => m
 | S p => S (plus p m)
 end.
Infix "+" := plus.
(* pour ce qui est des tactiques utilisées dans la preuve,
 j'utilise les même que dans la documentation de Idris *)
Theorem plus_assoc : 
 forall n m p, n + m + p = n + (m + p).
Proof.
 induction n.
 - simpl. trivial.
 - simpl. intros. rewrite IHn. trivial.
Qed.

Les preuves en Coq ou Idris peuvent se paraphraser ainsi :

On prouve le théorème par récurrence sur l'entier n.

• Si n = 0 alors après simplification il faut prouver que m + p = m + p ce qui est trivial.
• Ensuite si n = S n' alors il faut montrer S n' + m + p = S n' + (m + p), ce qui revient, par définition de la fonction plus, à montrer que S (n' + m + p) = S (n' + (m + p)) (c'est là l'appel à la tactique simpl qui effectue des réductions de calcul à partir de la définition de plus). Or, d'après l'hypothèse de récurrence on a n' + m + p = n' + (m + p), il suffit donc de montrer S (n' + (m + p)) = S (n' + (m + p)) (là c'est la série intros. rewrite IHn) ce qui est trivial.

Avec un peu de pratique, on peut factoriser les parties communes entres les deux cas de la preuve par récurrence est aboutir à cette preuve :

Theorem plus_assoc : 
 forall n m p, n + m + p = n + (m + p).
Proof.
 induction n; simpl; [|intros; rewrite IHn]; trivial.
Qed.

Les preuves se construisent pas à pas comme décrit dans la documentation de Idris et elles ne semblent pas plus compliquées à effectuer. Je dirais même que vu l'éventail de tactiques disponibles de base avec Coq, elle sont même sans doute plus simple. Exemple :

Require Import Omega.
Theorem thm1 :
 forall n m p, n <= m -> p + n <= p + m.
Proof.
 intros; omega.
Qed.

Ensuite, il y a un point qui me chagrine dans l'article de présentation de Edwin Brady. Au paragraphe 3.5 page 14, il écrit :

3.5 Metatheory
We conjecture that TT respects the usual metatheoretic properties, as shown in Figure 5.

Ici c'est moi qui graisse, parce que pour le Calcul des Constructions Inductives (qui est à Coq ce que TT est à Idris) on n'en est pas au stade de la conjecture mais d'un résultat établi. Est-ce bien une conjecture pour TT ou le résultat a été prouvé ?

De plus, même si je peux comprendre le choix fait pour contrôler si les fonctions définies sont totales ou partielles (paragraphe 3.6), il est plus strict que celui de Coq qui permet de définir des fonctions totales qui seront considérées (à tort) comme partielles par Idris (d'un autre côté en Coq il n'y a pas le choix : les fonctions sont toutes totales).

Pour apprendre en douceur et progressivement la programmation en Coq lorsque l'on vient de la programmation fonctionnelle sans type dépendant (Haskell ou OCaml, par exemple), à mon avis le plus simple est de lire le livre (en anglais) Software Foundations de Benjamin C. Pierce disponible en ligne avec le code associé. D'ailleurs le livre est écrit en Coq et la version htlm est générée via l'utilitaire coqdoc.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.