kantien a écrit 1131 commentaires

Et que penses-tu d'un modèle économique comme celui de OcamlPro pour leur produit alt-ergo ?
La version libre (sous licence CeCILL-C) est décalée d'un an par rapport à la version payante.

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

Et alors ? Avec moi il ne verrai pas grand chose : je viens déjà avec mon bulletin pris parmi ceux reçu par courrier, et il est plié en deux donc on ne voit pas ce qu'il y a dessus.
La seule chose qu'il verrait sur sa vidéo c'est moi mettant un papier dans une enveloppe. Pas très intéressant comme information. ;-)

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

Oups je me suis trompé. :-p
Ce sont les autorités possédant les clefs privées qui déchiffrent le résultat, et fournissent une preuve qu'elles l'ont correctement déchiffré. Les électeurs peuvent vérifier la validité de la preuve sans avoir besoin des clefs privées.

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

Le processus de dépouillement est expliqué dans cet articles sur interstices.
La validité du résultat proclamé, vérifiable pour tout le monde (et donc sans connaître le contenu de chaque bulletin), repose sur une propriété du chiffrement de El Gamal : il est homomorphique, c'est à dire que le produit des chiffrés est égale au chiffré de la somme. La somme correspondant au résultat des élections, et tout le monde ayant accès au chiffré de chaque bulletin, tout le monde peut peut calculer le chiffré du résultat et vérifier que le résultat proclamé est correcte.

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

Dans certains pays (cela dépend de la méthode de scrutin), il est possible de contraindre des électeurs sur leur choix de vote, même avec un isoloir à bulletin secret.
La méthode fût utilisée en Italie par la mafia dans les années 80, et elle semble avoir de nouvelles méthodes de nos jours.

Le principe est décrit dans l'article Attaque à l'Italienne de Véronique Cortier, et étudier plus en détail par Roberto Di Cosmo (connu pour ses pamphlets Piège dans le cyberespace et Le Hold-Up planétaire) dans cet article en anglais. L'idée consiste a utilisé la méthode de vote pour « signer » son bulletin, de telle sorte que la personne qui fait pression peut vérifier lors du dépouillement que sa consigne a été respectée.

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

Il faudrait demander son avis à Serge Dassault.
Il semblerait qu'il considère cela comme une méthode légitime pour remporter une élection. :/

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

Le choix de l'April est différent et compréhensible : il n'y a pas anonymat du vote, ce qui est le cas aussi pour les personnes présentes à l'AG qui votent à main levée. Ils font comme le projet Debian lors de l'élection du DPL.

Le fonctionnement d'Helios est différent : il garantie l'anonymat et la vérification (mais il n'y a pas de protection contre la coercition). Pour éviter le bourrage d'urne, il en existe une version évoluée appelée Belenios.

Le principe de fonctionnement est exposé dans l'article les bonnes propriétés d'un système de vote et plus en détail sur interstices. Dans le premier article, les auteurs n'en recommandent évidemment pas l'usage pour des élections institutionnelles, mais Helios sert pour l'élection du recteur de l'université catholique de Louvain, et l'association internationale des chercheurs en cryptographie pour l'élection de leur bureau (c'est autre chose que l'April).
Contrairement à un système papier que tout le monde comprend, et peut donc contrôler, le fonctionnement de ces systèmes est complexes et la compréhension réservée à une élite.

Même pour les systèmes les plus sûrs et les plus vérifiables, les mécanismes de vérification font appel à des théories mathématiques complexes dont la compréhension détaillée est réservée à des experts. Les autres utilisateurs doivent faire confiance à ces experts, contrairement au vote papier où les procédures sont comprises par une vaste majorité des citoyens.

les bonnes propriétés d'un système de vote

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

Véronique Cortier a récemment reçu le prix jeune chercheur Inria - Académie des Sciences pour ses travaux.

Sur le blog de la Société Informatique de France, elle a écrit une série de 4 articles sur le vote électronique :
Qu'est-ce qu'un bon système de vote ?
Les bonnes propriétés d'un système de vote électronique
Le vote papier est-il réellement plus sûr que le vote électronique
Attaque à l'italienne

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

Ça doit ressembler à ça :

PS4    Rpi   Freebox
 \      |     /
  \     |    /
   \    |   /
    \   |  /
      Ampli
        |
        |
      Télé

Il n'a besoin que d'une seule télécommande grâce au HDMI/CEC.
L'élément qui reçoit les ordres via la télécommande les retransmet aux autres via le câble HDMI (ils doivent être compatibles CEC pour cela).

Chez moi je n'ai que le Rpi dans le montage, et je commande Kodi avec la télécommande de ma télé.

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

J'entends bien, et n'ai pas soutenu le contraire (même si mon message pouvait le laisser sous-entendre). Dans tout contrat de cette sorte avec un prestataire (ici entre les pouvoirs publics et les opérateurs), les délais ne sont jamais respectés, il y a toujours du retard. Je faisais référence au consensus plus pour souligner que ce n'était pas une promesse en l'air, mais qu'elle devait avoir un fondement : en l'occurrence les engagements et accords préexistants à l'élection elle même. Cela permet d'avoir un ordre de grandeur assez fiable sur les délais (au minimum trois ans), ce qui était le seul point que je voulais souligner.

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

Dans mon canton, lors des dernières élections, les partis qui faisaient mention du déploiement de la fibre s'accordaient sur un horizon 2018 pour une couverture totale. J'en déduis que cela correspond sans doute à la réalité du processus enclenché, et que l'objectif sera probablement atteint (seule hypothèse crédible pour expliquer un consensus entre partis politiques rivaux). L'horizon est dans trois ans et il faut noter que je réside en Ile de France, donc pour la couverture nationale, on a le temps. ;-)

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

Ce qui confirme bien la conclusion du journal : ils sont à l'ère digitale; bien que personnellement je fasse usage de mon pouce et de mon index, en plus de mon majeur, afin de manipuler mon stylo. :-D

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

Soit, mais quand tu en es à te contenter d'un telle définition en format CD, tu n'en es pas à te poser les problèmes que tu considères (tu n'es pas une public professionnel, ni même amateur ;-)
Je ne critiquais en rien les apports de VP9 et H265.
Il y a des jours où je me demande si tu comprends ce que tu lis.

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

Cela étant, sur son cas pratique, si tu veux une hausse de 5O % du taux de compression sans perte de qualité, alors tu multiplies ton temps d'encodage par dix (cf partie encoding speed et deuxième graphique).

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

Question pertinente, systemd offre-t-il tous les contrôles possibles sur les cgroups ?
Thétis donne une indication dans son commentaire, ou bien l'usage que systemd en fait n'est pas complet ?

De ce que j'avais lu à l'époque (et compris), systemd avait recours aux cgroups pour sa gestion des processus (d'où l'impossibilité de port sur FreeBSD qui n'a pas cette notion).

P.S: tout comme pour rewind, nulle volonté trollesque dans ce message.

Edit : réponse juste au-dessus, merci gouttegd.

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

Il est vrai que le synopsis est mal présenté. Cette femme passait des heures à s'entraîner, elle a même fait appel à un professeur de chant, mais n'entendant pas sa fausseté c'était peine perdue : elle ne pourrait jamais chanter juste, quelque soit le temps qu'elle y consacrerait.

Pour toi c'est différent : lance-toi !! surtout si c'est une grande frustration de ta vie. Je suis aussi musicien (non multi-instrumentiste, juste guitariste), et pendant longtemps je n'ai pas chanté car j'entendais bien ma fausseté. Puis je me suis jeté à l'eau, j'ai pris un an de cours pour être encadrer, acquérir quelques techniques et de la méthode. Maintenant je suis loin d'être un grand chanteur, mais je ne chante plus faux.

Ta pratique des instruments a nécessairement développer ton oreille, cela te sera grandement profitable. Dans le même genre que le chant, nombre de guitaristes ne savent pas accorder leur instrument, ou ne se rendent pas compte qu'il est faux¹ : ça me bousille les esgourdes, question de quinte juste et c'est marre !!² ;-) Quand j'ai débuté, je ne m'en rendais pas compte non plus, maintenant j'identifie la corde en cause à l'oreille, et peut quasiment me passer d'accordeur.

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

Constat on ne peut plus vrai, bien que toujours attristant. À chaque fois que j'y repense, je ne peux que relire ceci :

Il n'est point de connaissance qui soit superflue et inutile de façon absolue et à tous égards, encore que nous ne soyons pas toujours à même d'en apercevoir l'utilité. C'est par conséquent un objection aussi mal avisée qu'injuste que les esprits superficiels adressent aux grands hommes qui consacrent aux sciences des soins laborieux lorsqu'ils viennent demander : à quoi cela sert-il ? On ne doit en aucun cas poser une telle question quand on prétend s'occuper de science. À supposer qu'une science ne puisse apporter d'explication que sur un quelconque objet possible, de ce seul fait son utilité serait déjà suffisante. Toute connaissance logiquement parfaite a déjà quelque utilité possible : même si elle nous échappe jusqu'à présent, il se peut que la postérité la découvre. Si en cultivant les sciences on n'avait jamais mesuré l'utilité qu'au profit matériel qu'on pourrait retirer, nous n'aurions pas l'arithmétique et la géométrie. Aussi bien notre intelligence est ainsi conformée qu'elle trouve satisfaction dans la simple connaissance, et même une satisfaction plus grande que dans l'utilité qui en résulte. Platon l'avait déjà remarqué. L'homme y prend conscience de sa valeur propre; il a la sensation de ce qui se nomme : avoir l'intelligence. Les hommes qui ne sentent pas cela doivent envier les bêtes. La valeur intrinsèque que les connaissances tiennent de leur perfection logique est incomparable avec leur valeur extrinsèque, qu'elles tirent de leur application.

E. Kant, Logique

Et puisque nous semble dans un lieu dédié principalement à l'informatique : qu'est-ce qu'on s'en fout de savoir si l'arithmétique est cohérente ?. Quoi que là, ce n'est pas la postérité qui a trouvé l'utilité, bien que l'on ne puisse savoir jusqu'où celle-ci ira… \o/

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

Je n'ai pas non plus de compte, et par chance n'est pas d'obligation d'en lire le contenu. Ma raison est simple : 140 signes c'est trop court, on ne peut rien dire. Encore que je peux admettre le principe pour signaler du contenu qui, lui, est développé en un autre lieu de la toile.

Mais là, si je comprends bien le principe : pour exprimer une pensée qui nécessite plus de 140 signes, on la découpe en morceaux que l'on envoie un par un pour que ça rentre dans la taille des boîtes ? :o L'espèce humaine m'étonnera toujours…

Pour la fédération, la notification temps réel, la décentralisation, etc. il me semble que XMMP et Pub-Sub le permettent allégrement. Le dossier de Goffi sur le sujet (fort passionnant, merci à lui) est instructif. Cela semble avancer, avec simplification de la XEP qui n'était pas complètement implémenter dans les serveurs car juger trop complexe (bien qu'après lecture de la XEP, je ne vois pas ce qu'il y a de compliqué dedans).

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

De rien messieurs, j'espère n'avoir pas été trop confus, ni trop abstrait dans ma présentation. Je viens de commencer la thèse de Perthmâd, et dans ses prolégomènes vous pourrez y trouver une exposition plus détaillée du sujet. On y trouve en particulier :

• les règles de typage du lambda calcul simplement typé (sans variants, ni tuples) à la page 25 ;
• celles du lambda-calcul avec variants et tuples à la page 27 ;
• les règles d'inférences de la logique propositionnelle intuitionniste page 30.

Puis en haut de la page 33, il montre l'identité formelle entre deux sous-ensembles de ces règles (ce en quoi consiste la correspondance de Curry-Howard) sous la forme d'un tableau de deux lignes et quatre colonnes (la quatrième correspondant à ce que j'ai dit au sujet du modus ponens). Pour les autres règles, il vous suffit de les comparer vous même.

Quelques compléments pourront vous être utiles pour comprendre certaines de ses notations. D'abord sur le lambda-calcul, vous n'avez qu'à lire le lambda-terme Lx.t (le L remplace le lambda minuscule) comme l'expression OCaml fun x -> t. Enfin pour ce qui est du lien entre multiplication-conjonction et addition-disjonction (type produit et type somme), constatez que A et (B ou C) = (A et B) ou (A et C) : loi de distribution comme dans les anneaux. Cette idée vient de la théorie générale des algèbres de Boole que l'on peut définir comme des corps dans lesquels tout élément est son propre carré (A et A = A) : l'algèbre de Boole a deux éléments (true et false) étant la plus simple de toutes.

Pour information, le principe de cette correspondance peut être étendu au typage de protocole réseau. Le prix jeune chercheur INRIA a été attribué à Véronique Cortier qui travaille, entre autre, sur le projet Belenios (système sécurisé de vote en ligne); système qui cherche un développeur OCaml pour le développement de sa plateforme Web : c'est pas un truc cool en France ?! ;-)

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

Pour le code le fonction pred, il faut bien sûr lire

let pred n =
  match n with
  | Zero -> None
  | S n' -> Some n'

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

Au sujet du « faux », ne penses-tu pas que les développeurs OCaml peuvent utiliser le type polymorphe 'a option pour représenter cette notion ? L'idée m'est venue en relisant l'article du programme de Hilbert aux programmes tout court de Jean-Louis Krivine, en particulier ce passage au sujet de la correspondance de Curry-Howard :

Ce sont des logiciens qui l'ont découverte, tout au moins en ce qui concerne la logique intuitionniste. Mais c'est un informaticien, T. Griffin qui a opéré son extension à la logique classique, trente ans après, en 1990. C'est, de nouveau, une découverte capitale et tout à fait inattendue : en effet, le raisonnement par l'absurde est associé à une instruction très sophistiquée du langage SCHEME (une variante de LISP), qui a été inventée pour gérer, entre autres, les exceptions et le multi-tâches.

Or le type 'a option est une manière de gérer les exceptions de manière plus fonctionnelle en OCaml que de lever une exception de type exn. Je m'explique sur l'exemple du calcul du prédécesseur pour les entiers unaires :

type nat = Zero | S of nat

let pred n =
  match n with
  | Zero -> None
  | S n' -> n'

Un entier qui aurait zéro pour successeur est absurde, mais pas pour les autres entiers. Cela se passe comme si lorsque l'hypothèse est absurde on renvoie None, alors que lorsque ce n'est pas le cas on renvoie une conclusion du bon type Some 'a. Ce qui me fait penser à l'interprétation gödelienne de la logique intuitionniste : dans chaque étude de cas, on dispose soit d'une preuve de l'absurdité de l'hypothèse, soit de la prouvabilité du théorème sous l'hypothèse donnée. Cette interprétation te semble-t-elle recevable ? Les leçons de M. Krivine sont trop lointaines pour moi (une dizaine d'années, et déjà à l'époque je n'avais suivi son cours sur le lambda-calcul typé qu'en option) pour que je puisse avancer avec assurance sur ce genre de question.

Autrement, je viens de commencer la lecture de ta thèse et j'apprécie beaucoup ton sens de l'humour :-) En conclusion des remerciements, tu en adresses à Jean-Yves et Jean-Louis, que je suppose être MM. Girard et Krivine. J'aurais aimé me procurer les deux tomes de l'ouvrage Le point aveugle, mais le premier tome est en rupture de stock chez tous les distributeurs que j'ai regardé. Sais tu s'il en est prévu une réédition ?

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

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.

Effectivement, la force des langages comme OCaml ou Haskell est la puissance sémantique de leur système de types. Outre la garantie qu'il n'y aura pas d'erreurs de typage à l'exécution (ce qui était ici reproché à python, mais ne les distingue pas de langage comme le C si l'on passe sous silence l'absence d'effets de bord), le système est un sous-ensemble riche du calcul propositionnel du second ordre : ce qui offre de plus un bon contrôle sémantique sur le code, mais ne dispense pas des tests unitaires.
Pour se dispenser complètement de ces derniers, il faut passer à Coq qui lui à tout le calcul des prédicats du second ordre avec logique intuitionniste (sans raisonnement par l'absurde, quoi que on peut même activer ce dernier mais là…).
Pour ceux qui ne connaissent pas ces notions, disons qu'on peut par exemple exprimer dans le système de types de Coq que l'on définit une fonction qui prend un entier et renvoie son double. Autrement dit on peut exprimer complètement la sémantique du code, et le système vérifie que le code correspond bien à sa sémantique. D'une certaine façon, un code Coq qui compile est garantie sans bugs.

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

Pour le web que reproches tu à Ocsigen et pour le xml à la bibliothèque xmlm ?
Il me semble d'ailleurs que Ocsigen utilise cette dernière pour la production du code html, dont la bonne formation est garantie par le système de type de OCaml (pas de besoin du html validator).
Le projet Ocsigen développe aussi js_of_ocaml pour compiler du code Ocaml vers javascript (et qui tourne des fois plus vite que du bytecode OCaml), ce qui permet par exemple de faire tester des programmes OCaml dans un navigateur comme le font OCaml Pro avec leur logiciel alt-ergo.

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

Tu as parfaitement raison de le souligner. En fait je reprenais dans mon message les termes même du message que je citais, pour des raisons de continuité; je n'aurai peut être pas du.

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