Re: Le web

Pour la taille des programmes que les spécialistes de Coq peuvent écrire, je pense que la réponse de Perthmâd est suffisante. Quand je parle de spécialistes, il faut voir que pour le compilateur C il s'agit d'un projet de Xavier Leroy, le Big Boss OCaml.
On pourrait rajouter un micro noyau, mais lui certifié par Isabelle.

Pour le reste de tes questions, je veux bien essayer de répondre, en espérant rester le plus compréhensible possible. En guise d'avertissement, je tiens à préciser que je ne suis ni informaticien, ni développeur, par contre tout comme toi je suis mathématicien de formation, mais également logicien (master Logique Mathématique et Fondements de l'Informatique) porté sur la philosophie (d'où mon pseudonyme).

Tout d'abord, en logique on distingue la partie qui traite des règles de bonne formation des jugements (règles syntaxiques) de celle qui s'occupe des règles par lesquelles on dérive ou infère les jugements les uns des autres (théorie de la démonstration). Les notions de logique propositionnelle ou des prédicats du premier ou second ordre relèvent de la première partie, alors que la distinction entre logique intuitionniste ou classique de la seconde. Je présenterai d'abord quelques notions syntaxiques, puis dans un second temps la différence entre logique classique et intuitionniste, et enfin je tenterai de montrer les liens entre ces notions et le typage de programme.

Lorsque l'on s'intéresse à la forme logique de nos jugements, quelqu'en soit le contenu (il fait beau, mon pseudonyme est kantien, Socrate est mortel, Gödel est le plus grand logicien du vingtième siècle, Kant est le plus grand philosophe de tous les temps...), si l'on fait abstraction du rapport sujet-prédicat (la structure sujet-verbe-complément) on trouve qu'ils se subdivisent en jugements affirmatifs (il fait beau), négatifs (il ne fait pas beau), hypothétiques (s'il fait beau alors je vais me promener), conjonctifs (il fait beau et les oiseaux chantent) ou disjonctifs (il fait beau ou il pleut). Tel est le point de vue de la logique propositionnelle. Usuellement, on représente les propositions non analysées, à partir desquelles on construit toutes les autres, par des lettres majuscules A, B, C... À partir d'elles on peut former, par exemple, les jugements : A et B et C, non A ou B, si A alors B etc. Cela doit paraître clair et évident pour un développeur : ce sont tous les opérateurs agissant sur les booléens. Mais pour l'instant on en reste à la logique propositionnelle dite du premier ordre : on ne se permet pas de quantifier sur les variables propositionnelles (aucun article défini ou indéfini, singulier ou pluriel). Quand on autorise une telle quantification, on parle de logique propositionnelle du second ordre. Dans une telle logique, on peut former des propositions de la forme : Pour toutes propositions A,B si A alors B. On note habituellement la forme des jugements hypothétiques (ou implication) par une flèche ->, et la proposition précédente se réécrit Pour toutes A,B A -> B. En anticipant la partie sur le typage, tu pourras comparer au type OCaml 'a -> 'b ;) (l'apostrophe ' a son importance, c'est le quantificateur universel).
Voilà qui est bien intéressant, mais dans nos phrases nous utilisons des verbes, et la grammaire ne répète-t-elle pas que la phrase minimale est constituée de la structure sujet-verbe-complément ? Les logiciens préfèrent parler de rapport sujet-prédicat ou de rapport prédicatif entre un ou plusieurs sujets. On parle alors de logique des prédicats. Ainsi, dans la phrase « Socrate est mortel » Socrate est le sujet, mortel le prédicat; tandis que dans la phrase « Roméo aime Juliette » aimer est le prédicat Roméo et Juliette en étant les sujets (on parle de prédicat binaire). Tout comme pour la logique propositionnelle, on distingue un premier et un second ordre selon les objets sur lesquels on autorise la quantification : quand on ne quantifie que sur les sujets on est au premier ordre, tandis que si l'on quantifie aussi bien sur les sujets que sur le prédicats on est au second ordre. Je vais tâcher d'illustrer la différence entre ces deux ordres dans la formulation des théories en prenant l'exemple de l'arithmétique.
Lorsque l'on cherche à axiomatiser l'arithmétique (comme il se doit pour toute théorie mathématique), outre les axiomes de bases comme 0 est un entier, tout entier a un successeur, le successeur d'un entier n'est jamais nul... il faut pouvoir exprimer l'essence même des nombres entiers : le principe du raisonnement par récurrence. En première année de licence, on le présente ainsi : si un proposition est vraie de 0 et qu'elle passe au successeur (si elle est vraie pour n alors elle est vraie pour n+1) alors elle est vraie pour tout entier. On pourrait l'écrire aussi : Pour tout P, (P0 et (Pn -> P(n+1))) -> pour tout n, Pn. Dans une telle formulation, la quantification porte aussi bien sur les propositions que sur les entiers : elle est du second ordre. Par contre, dans la logique du premier ordre on ne peut quantifier sur les propositions, il faut s'y prendre autrement. Alors, au lieu d'un unique axiome, on pose une infinité d'axiomes à travers ce que l'on nomme un schéma d'axiomes : à chaque proposition syntaxiquement bien formée (P) portant sur les entiers, on lui associe son axiome de récurrence : si P est vraie de 0 et qu'elle passe au successeur... La théorie a beau avoir une infinité d'axiomes, elle reste récursivement énumérable : il existe un algorithme pour décider si une formule est ou non un axiome. Par contre il n'existe pas d'algorithme pour décider si une formule est une conséquence déductive de la théorie : tel est le premier théorème d'incomplétude de Gödel (qui a pour corollaire l'impossibilité de résoudre le problème de l'arrêt pour une machine de Turing). Ce qui nous amène à la deuxième partie : qu'est-ce qu'être une conséquence déductive ? ou qu'elles sont les règles pour prouver ?

Je n'entrerai pas dans le détail de toutes ces régles, ni dans un exposé exhaustif, mais m'arrêterai sur trois règles qui ont leur importance dans la différence et l'opposition entre logique classique et intuitionniste : le modus ponens, le modus tollens et le tiers exclus. La première peut s'exprimer dans le raisonnement suivant : si A alors B, or A donc B. La seconde dans le raisonnement suivant : si A alors B, or non B donc non A (on parle aussi de raisonnement par contraposition : la contraposée de la proposition si A alors B étant la proposition si non B alors non A, le modus tollens n'est que le modus ponens appliqué à la contraposée). Enfin, la troisième affirme que pour toute proposition A, on peut poser A ou non A (entre une thèse et son antithèse, tout tiers est exclus). Et c'est cette dernière règle que les intuitionnistes rejètent : elle permet de prouver l'existence d'objets sans même exhiber un moyen de les construire (on a pour cela qualifié les intuitionnistes de constructivistes). Illustrons cette propriété étonnante du tiers exclus sur un exemple célèbre.
Théorème : il existe deux nombres irrationnels a et b tels que a^b soit rationnel.
Preuve :
Posons a = b = racine de 2 qui est irrationnel. Selon le tiers exclus, ou bien a^b est rationnel ou bien il ne l'est pas, c'est à dire qu'il est irrationnel. Si le premier cas est vrai, alors on a fini. Supposons donc que a^b soit irrationnel. Alors comme (a^b)a = a^b*a = a² = 2 est rationnel, il suffit de prendre a^b et a pour les deux nombres cherchés.
CQFD.
Voilà une preuve bien étrange : elle affirme l'existence de deux nombres ayant une propriété particulière, mais à la fin de la preuve on ne les connaît pas, ne sachant pas laquelle des deux alternatives fournies par le tiers exclus est la bonne. À dire vrai, on peut prouver sans tiers exclus que la deuxième alternative est vraie... mais la preuve est bien plus longue. ;)
Le principe du tiers exclus est équivalent au principe du raisonnement par l'absurde que l'on peut formuler ainsi : (non A -> A) -> A. Autrement dit : si une antithèse prouve la thèse qu'elle est censée réfuter, alors on peut affirmer la thèse sans hypothèse auxiliaire. Une des conséquence surprenante de la logique intuitionniste est qu'une double négation n'est pas équivalente à une affirmation ( non non A n'est pas équivalente à A). Dans un raisonnement par l'absurde, un intuitionniste conclura à la double négation (non A -> A -> non non A) mais non à l'affirmation comme le ferai un mathématicien « classique ». De même, si le principe du tiers exclus n'est pas prouvable en logique intuitionniste, on peut par contre y prouver la double négation de celui-ci.

J'espère que la réponse sur la traduction des « pour tout » et la nature du second ordre te semble claire : les intuitionnistes traduisent comme tout le monde, le second ordre permet de quantifier sur les prédicats, mais les intuitionnistes ne concluent pas toujours comme le font les mathématiciens « classiques ». C'est dans les liens logico-déductifs entre énoncés, et non dans leur formulation, que se situe la différence entre logique classique et logique intuitionniste.
Venons en enfin aux programmes et à leur typage, et donc à la correspondance de Curry-Howard ou correspondance preuve-programme (là où tu t'es dis « chouette » ;). Les langages fonctionnels comme OCaml (ou Haskell, Lisp...) ont pour modèle théorique le lambda-calcul, là où les langages impératifs s'inspirent du modèle des machines de Turing. Le lambda-calcul d'Alonzo Church avait pour ambition de capturer l'essence de la notion mathématique de fonction ¹ . Le lambda-calcul peut être vu comme un langage de programmation, dans lequel les fonctions sont des citoyens de première classe, où les types sont des formules du prédicats du seconde ordre: telle est la correspondance de Curry-Howard. Cela est du au fait que les règles de typage de ce langage sont analogues aux règles de déduction de la logique intuitionniste. Ainsi, en gros, à chaque fois que l'on type un lambda terme on peut construire en parallèle une preuve d'un théorème : le théorème « dit » ce que fait le programme ² , et celui-ci est une preuve particulière de celui-là.
Prenons des exemples avec le typage de fonctions en Ocaml. Si l'on définit la fonction let f x = x +1, elle aura pour type int -> int et quand on calcule le terme f 1 on trouve la valeur 2 de type int. Observes bien la forme du type de la fonction ! Ne te rappelle-t-il pas la notation de l'implication logique A -> B (si A alors B) avec ici A = B = int ? C'est bien le cas. Le type int peut être vu comme une constante propositionnelle, et le type de la fonction f comme la tautologie si A alors A. Et quand on l'applique a une valeur du bon type, on applique la règle du modus ponens : si A alors A, or A donc A (1 est de type int, le or A, donc la valeur f 1 = 2 est de type int). La forme générale du modus ponens s'obtient avec la fonction let apply f = fun x -> f x de type ('a -> 'b) - 'a -> 'b que l'on peut paraphraser en : Pour toute proposition A et B, si A alors B or A donc B. On a là une formule du second ordre, et c'est ce second ordre qui confère le polymorphisme au langage. Les fonctions et leur application permettent donc de retrouver les formules hypothétiques. Pour ce qui est des formules disjonctives et conjonctives, elles sont fournies respectivement par les variants et les enregistrements (les variants sont des « ou », les enregistrements des « et »). Comme il manque la négation logique, on retrouve un sous-ensemble de la logique propositionnelle du second ordre. Ainsi, si on regarde les fonctions OCaml comme des preuves et leur type comme des théorèmes, le compilateur vérifie que l'on applique les théorèmes à des prémisses dont la forme est conforme à l'énoncé du théorème : autrement dit, on n'utilise pas les théorèmes n'importe comment, comme quelqu'un qui voudrait appliquer le théorème de Pythagore à un triangle équilatéral.
Malheureusement, ce système est limité quand à son expressivité sémantique : il n'y a pas de prédicats. C'est là que Coq entre en jeu. Pour un programmeur, y avoir recours peut être disproportionné (sortir un char d'assaut pour tuer une mouche), mais dans des logiciels critiques où le droit à l'erreur n'est pas permis (comme le pilote automatique d'un avion ;) cela peut s'avérer être une solution recevable. Je vais illustrer son principe en utilisant un exemple donné par Perthmâd dans son article sur coq 8.5. Il y définit une fonction qui calcule le nombre d'occurrence d'un entier dans une liste, et prouve que si on concatène deux listes on ajoute le nombre d'occurrence.

(* import de modules pour les listes et l'arithmétique *)
Require Import List Arith.
Fixpoint multiplicity (n : nat) (l : list nat) : nat :=
 (* filtrage par motifs sur la liste "l" *)
 match l with 
 (* cas où la liste est vide *)
 | nil => 0 
 (* cas où on a un élément "a" en tête de liste, "l'" le reste *) 
 | a :: l' => 
 (* test d'égalité de "n" avec l'élément "a" *) 
 if eq_nat_dec n a 
 (* appel récursif suivi de la fonction successeur d'un entier *)
 then S (multiplicity n l') 
 else multiplicity n l' 
 end.
Lemma multiplicity_app (n : nat) (l1 l2 : list nat) : 
 multiplicity n (l1 ++ l2) = multiplicity n l1 + multiplicity n l2.
Proof.
 induction l1. reflexivity.
 simpl. destruct eq_nat_dec; auto.
 rewrite IHl1. auto.
Qed.

En OCaml, cela ressemblerai à ceci :

(* représentation unaire des entiers naturels *)
type nat = Zero | S of nat;;
(* prédicat d'égalité décidable entre deux entiers *)
let rec eq_nat_dec n m =
 match n, m with
 | Zero, Zero -> true
 | Zero, _ | _, Zero -> false
 | S n', S m' -> eq_nat_dec n' m'
;;
(* la fonction multiplicity définie comme en Coq *)
let rec multiplicity n l =
 match l with
 | [] -> Zero
 | a :: l' ->
 if eq_nat_dec a n
 then S (multiplicity n l')
 else multiplicity n l'
;;
(* définition de l'addition sur le type nat *)
let rec plus_nat n m =
 match n, m with
 | Zero, _ -> m
 | _, Zero -> n
 | S n', S m' -> S (S (plus_nat n' m'))
;;
(* morphisme du type int vers le type nat *)
let rec nat_of_int n =
 match n with
 | 0 -> Zero
 | _ -> S (nat_of_int (n-1))
;;
(* morphisme du type nat vers le type int *)
let rec int_of_nat n =
 let rec loop m acc =
 match m with
 | Zero -> acc
 | S m' -> loop m' (acc + 1)
 in loop n 0
;;

On remarque déjà que le théorème ne porte pas sur le type int mais sur le type nat. D'ailleurs, le type int muni de l'addition est un groupe cyclique isomorphe à un Z/nZ où la valeur de n dépend de l'architecture de la machine (2³¹ sur 32-bit et 2⁶³ sur 64-bit), et ne représente qu'imparfaitement le concept de nombre entier. Toutefois, en utilisant les morphismes entre les deux types on pourrait le « traduire » pour le type int.
Et dans une boucle interactive :

(* on représente 2 en unaire *)
# let n = nat_of_int 2;;
val n : nat = S (S Zero)
(* on crée deux listes d'entiers unaires qu'on concatène *)
# let l1 = List.map (nat_of_int) [2; 3; 4; 2; 5];;
val l1 : nat list =
 [S (S Zero); S (S (S Zero)); S (S (S (S Zero))); S (S Zero);
 S (S (S (S (S Zero))))]
# let l2 = List.map (nat_of_int) [2; 3; 4; 2; 2];;
val l2 : nat list =
 [S (S Zero); S (S (S Zero)); S (S (S (S Zero))); S (S Zero); S (S Zero)]
# let l3 = l1 @ l2;;
val l3 : nat list =
 [S (S Zero); S (S (S Zero)); S (S (S (S Zero))); S (S Zero);
 S (S (S (S (S Zero)))); S (S Zero); S (S (S Zero)); S (S (S (S Zero)));
 S (S Zero); S (S Zero)]
(* le théorème est bien vérifié sur ce cas particulier *)
# multiplicity n l3 = plus_nat (multiplicity n l1) (multiplicity n l2);;
- : bool = true

Là où pour vérifier la correction sémantique de la fonction un développeur OCaml ferai des tests unitaires (qui ne seront jamais exhaustifs étant donné qu'il faudrait tester une infinité de cas), la preuve en Coq nous garantie qu'elle est correcte. Comme dit plus haut, avoir recours à Coq pour cet exemple est sans doute disproportionné par rapport au besoin. Un cas plus proche de la pratique est, par exemple, cette structure de données union-find persistante.

Si tu as eu la patience de rester en ma compagnie jusqu'au bout, et que je n'ai pas fait trop d'erreurs ou contresens (ces cours sont loin pour moi, Perthmâd me corrigera sans doute sur quelques points), j'espère t'avoir fait entrevoir les théories mathématiques qui se cachent aux fondements de OCaml. Pour la correspondance de Curry-Howard, comme référence accessible en ligne tu as Lambda-calculus, types and models de Jean-Louis Krivine. En ce qui concerne le système Coq, il y a un ouvrage collaboratif Homotopy Type Theory (sous creatives-commons, écrit en utilisant git) ou cet article sur le site Images des Maths du CNRS.

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