kantien a écrit 1198 commentaires

C’est clair que personnellement j’aurais été au bureau de vote insister pour mettre une enveloppe dans l’urne en collant ce courrier sous le nez des assesseurs…

Ça tombe bien c'est à cela qu'il sert ce papier : te permettre de voter en t'inscrivant sur les listes par décision du juge.

Le juge du tribunal d'instance, directement saisi, a compétence pour statuer jusqu'au jour du scrutin sur les réclamations des personnes qui prétendent avoir été omises sur les listes électorales par suite d'une erreur purement matérielle ou avoir été radiées de ces listes sans observation des formalités prescrites par les articles L. 23 et L. 25.

Article L. 34 du Code électoral

Ou encore :

L’article L. 34 du code électoral permet aux électeurs de demander leur inscription au juge du tribunal d’instance jusqu'au jour du scrutin en cas d'omission par suite d'une erreur purement matérielle ou en cas de radiation sans observation des formalités prescrites aux articles L. 23 et L. 25 du même code.

Circulaire du 14 février 2014 relative aux élections municipales, p. 6

Il est vrai que c'est assez amusant d'écrire un journal prétendant que des électeurs n'ont pu voté à cause d'erreurs matérielles, en l'illustrant par un document qui prouve le contraire…

Même si je pense qu’on ne m’aurait pas laissé voter, on m’aurait entendu !

Bah si, toute personne en possession d'un tel document a pu voter ! :-)

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

D'un autre côté, il y a un point qui me chagrine entre les deux contrats : celui de licence GPL et le contrat de service de fourniture de patchs. Le second semble conditionné à une clause de non divulgation du code, or c'est précisément ce type de clause qui a conduit RMS à créer la GPL et cela selon le droit américain. Les différentes versions de la GPL s'y seraient-elles mal prises pour atteindre leur but premier : éviter les clauses de non-divulgation ?

On peut faire du copyleft-left, pour revenir à du copyright ? Je ne sais si les questions sont orthogonales, mais ça m'a l'air complexe tout ça ! :-P

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

C'est quoi les "referers"? Merci.

Quand tu arrives sur une adresse via un lien, cela dit quelle est l'adresse de la page contenant le lien : cela informe le site que tu visites de l'endroit d'où tu viens (cf referer). Certains personnes les désactivent pour ne pas être « tracées ».

Je suppose, dans le cas du vote, que c'est pour contrôler que l'on arrive bien sur une de leurs pages en suivant pas à pas leur procédure.

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

Elle a été rajoutée par la modération, j'avais fait un copier/coller des données du site Debian qui ne comportent pas le symbole %. Cette fois, c'est pas moi ! :-P

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

La webui est-elle responsiv?

Elle l'est, c'est écrit dans la dépêche à la section ergonomie de l'interface web :

La version 4.0 fut l’occasion parfaite de rajeunir l’image de Rudder en lui offrant une nouvelle interface, plus moderne et responsive.

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

La voix blanche a toujours eu du mal à se faire entendre, tandis que la voie blanche fait le bonheur des contemplateurs d'étoiles. :-)

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

L'expérience a été présentée dans un journal il y a une semaine, mais il faut être inscrit sur facebook : c'est pas pour moi. ;-)

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

Merci pour l'information, la démarche du site me plaît je vais y participer. Il manque quelques scrutins que j'aurais bien aimé expérimenter mais ils ont fait le choix, compréhensible, de prendre des scrutins facile à expliquer (d'autant qu'ils mèneront également des expérimentations dans cinq bureaux de vote dimanche).

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

Je me renseigne sur la compatibilité avec le noyau Linux… :-)

Oui renseigne toi bien, mais pas que sur la compatibilité noyau. Sur une des mes machines je n'ai pas de problème de compatibilité hormis un firmware non libre pour le wifi (mais ça, c'est quasi mission impossible de faire sans avec ce type d'offre), néanmoins j'ai eu un autre soucis pour y installer ma Debian : le BIOS. :-/

Il m'était impossible faire booter ma machine sur une clé usb d'installation. Pour cela, il m'a fallu d'abord accepter l'installation de Windows 10 pour mettre à jour le BIOS (le problème était connu et un BIOS à jour était mis à disposition sur le site d'Acer), pour ensuite virer le Windows que je venais d'installer en le remplaçant par une Debian. Le problème datant de 2-3 ans, il est fort probable qu'il n'existe plus sur des Acer d'aujourd'hui, mais on ne sait jamais.

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

Premièrement, le mode de scrutin est celui prévu par la constitution du projet. Deuxièmement, si j'ai fait allusion à la méthode de Condorcet bien qu'il n'y ait que deux candidats, c'était plus comme un clin d'œil à certains journaux publiés dernièrement. Troisièmement, dans la mise en pratique par Debian, même avec deux candidats, il y a trois options sur le bulletin de vote : ils rajoutent l'option « aucun des deux » (constitution 5.2.6); ce qui ne se limite pas à une simple prise en compte du vote blanc, comme le montre le calcul de la majorité pour chacun des candidats. Enfin, dans une telle situation, la différence entre scrutin uninominal et méthode de Condorcet relève effectivement du pinaillage et de l'onanisme intellectuel.

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

Ou que le courrier contient bien le bulletin mis par le votant. La technique du MITM n'est pas propre aux communications électroniques.

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

Aucune idée, je ne suis qu'utilisateur et non développeur Debian. Je ne suis pas de près ce qui se passe au sein du projet.

Sinon Mehdi (ça y est, j'ai bien écrit son prénom ! \o/) n'a occupé ce poste que durant une année (2016-217), et tu peux te faire une idée de son action à partir des comptes rendus qu'il a faits sur leur mailing-list.

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

Je viens de m'apercevoir que j'ai écorché le nom d'un des candidats : le DPL sortant s'appelle Medhi (et non Medi) Dogguy.

Toutes mes confuses.

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

Je ne sais pas comment on est arrivé au modèle actuel, mais je vois bien pourquoi on n'a pas pu le changer jusqu'à maintenant:

Les 2 plus gros partis, qui gagnent alternativement quasiment toutes les élections, n'ont absolument aucun intérêt à changer un système qui favorise… les 2 plus gros partis!

Il se peut que tu prennes là l'effet pour la cause. Le mode de scrutin uninominal ne peut parfaitement représenter la volonté majoritaire qu'en la présence de deux alternatives, raison pour laquelle il pousse aux alliances et au bipartisme.

Pour ce qui est des raisons qui ont amené ce modèle, il se peut que ce soit de bêtes problèmes d'ordre logistique. De mémoire, Condorcet et Borda, qui avait fort bien analysé les problèmes de ce mode de scrutin, dans leurs mémoires où ils exposaient des méthodes alternatives ont pointés du doigt la plus grande complexité d'organisation du vote selon leur principe. Cela étant, cela n'a nullement empếché d'autres pays de s'en inspirer et de ne pas pratiquer le scrutin uninominal.

Enfin, pour l'anecdote, je n'ai plus grand espoir de voir le mode de scrutin changer en France, mais on ne sait jamais. Lors de l'élection de 2002 j'avais prévenu mon entourage des dangers que représentait le grand nombre de candidats au premier tour et le risque d'éparpillement des voix; j'ai obtenu pour réponse : la politique c'est pas des mathématiques ! Suite au résultat du premier tour, aucune prise de conscience : le mode de scrutin ne pose aucun problème. Dans la foulée, un ami qui effectuait sa thèse en science politique organise une conférence avec politologues et sondeurs (qui défendaient leur chapelle sur leurs « erreurs de prédiction ») pour essayer d'analyser et de comprendre le résultat de l'élection. Au moment des questions du public, rebelote, je remets sur le tapis la question du mode de scrutin et là, réaction identique et unanime : où est le problème avec notre mode de scrutin ? il n'y a aucune raison de le changer !

Je doute, par expérience, que la résistance au changement proviennent des deux gros partis, mais bien plutôt des électeurs eux-mêmes qui ne voient pas que le mode de scrutin pose problème.

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

Tu sembles ignorer un peu les sources d'informations contradictoires. Mais c'est un choix courant à notre époque.

Pour continuer à t'aider dans l'équilibre des sources d'informations, voici une autre vidéo issue de la même chaîne que la tienne : Mélenchon, hommage à Fidel Castro. Et quel grand démocrate ce Fidel !

Mais il est vrai que l'on peut y déceler toute la subtilité de Jean-Luc, ce fin rhéteur, lorsqu'il fustige l'embargo portant sur 20% de l'économie cubaine (vers 3min 30). En effet, comment ne pas lire entre ligne et constater que, sous des faux semblants, il cherche en réalité à faire l'éloge du libre-échange entre les nations. :-D

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

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.

Certes, mais même lorsque l'on fait du typage statique et que l'on utilise un algorithme d'unification, il est possible de renvoyer des messages plus compréhensibles. Le papier auquel tu renvoies donne des pistes, mais le message de Guillaume Denry sur elm est encore plus parlant. Elm a un système de type à la Haskell et son message d'erreur est on ne peut plus compréhensif et informatif.

Comme ces derniers temps je joue un peu avec Coq, qui doit faire face à des problématiques d'unification à coté desquelles celles de Rust sont un jeu d'enfant, je vais donner des exemples dans ce langage.

Pour commencer, il semblerait naturel de n'utiliser une notation infixe x + y que dans une structure de monoïde. Alors je vais le faire façon type classes à la Haskell :

Class monoid {A : Type} (op : A -> A -> A) (e : A) := {
  _ : forall x y z, op x (op y z) = op (op x y) z ;
  _ : forall x, op e x = x ;
  _ : forall x, op x e = x }.

Generalizable Variables A op e.

Definition monoid_op `{M : monoid A op e} x y := op x y.

Infix "+'" := monoid_op (at level 50).

Là on fait un type checking sur la fonction monoid_op :

Check monoid_op.
(* ==>
monoid_op
     : ?A -> ?A -> ?A
where
?A : [ |- Type] 
?op : [ |- ?A -> ?A -> ?A] 
?e : [ |- ?A] 
?M : [ |- monoid ?op ?e] *)

Elle prend deux valeurs d'un certain type ?A et renvoie une valeur de ce type, et cela dans un contexte où ce type est connu avec un monoïde sur les valeurs de ce type (le ? signifie que le terme est indéterminé, la variable est existentielle : il existe une valeur A telle que …). Si on lui demande de typer l'expression 1 +' "3a", on obtient :

Check 1 +' "3a".
(* ==>
Error:
The term ""3a"" has type "string" while it is expected to have type "nat". *)

Mais le plus amusant est qu'il peut typer le terme "1" +' "3a" avant même de savoir le calculer :

Check "1" +' "3a".
(* ==>
"1" +' "3a"
     : string
where
?op : [ |- string -> string -> string] 
?e : [ |- string] 
?M : [ |- monoid ?op ?e] *)

Eval compute in "1" +' "3a".
(* ==>
     = ?op "1" "3a"
     : string *)

Maintenant pour lui permettre de calculer, on lui fournit une instance de la classe :

(* on prouve que le type string muni de l'opération de concaténation
   est un monoïde dont l'élément neutre est la chaîne vide. *)
Instance Str_append : monoid append "".
Proof.
split.
- induction x; [auto | intros; simpl; rewrite IHx; reflexivity].
- reflexivity.
- induction x; [auto | simpl; rewrite IHx; reflexivity].
Qed.

(* maintenant on vérifie le type et on évalue : *)
Check "1" +' "3a".
(* ==>
"1" +' "3a"
     : string *)

Eval compute in "1" +' "3a".
(* ==>
     = "13a"
     : string *)

Pour le cas plus général où les deux opérandes ne sont pas du même type (et l'on se demande bien alors pourquoi utiliser la notation additive ?), et revenir à la situation de python, je vais l'illustrer ainsi.

Class bin_op (A B C : Type) := op : A -> B -> C.

Infix "+'" := op (at level 50).

Check 1 +' "3a".
(* ==>
1 +' "3a"
     : ?C
where
?C : [ |- Type] 
?bin_op : [ |- bin_op nat string ?C] *)

Là on est dans la situation de python : comme il fait du typage dynamique, lors de l'appel au calcul de l'expression il vérifie si l'environnement permet de bien typer le terme (s'il peut instancier ces variables existentielles). Comme ce langage permet de modifier dynamiquement l'environnement, il est impossible de refuser statiquement ce code. Il pourrait, par exemple, être défini dans une bibliothèque où le code ne peut être évalué, puis importer dans un code qui rend l'évaluation possible. Comme dans le dialogue suivant avec la REPL Coq :

Eval compute in 1 +' "3a".
(* ==>
     = ?bin_op 1 "3a"
     : ?C *)

(* ici l'évaluation totale génère une erreur : le typage étant statique,
   il exige d'être dans un environnement où les variables existentielles
   sont instanciées. *)
Eval vm_compute in 1 +' "3a".
(* ==>
Error: vm_compute does not support existential variables. *)

Instance nat_add : bin_op nat nat nat := {op := plus}.
Instance str_app : bin_op string string string := {op := append }.
Instance nat_str : bin_op nat string string := {
  op n s:=
    match get n s with 
    | None => ""
    | Some c => String c ""
    end }.

Eval vm_compute in 1 +' 3. (* ==> 4 : nat *)
Eval vm_compute in "1" +' "3a". (* ==> "13a" : string *)
Eval vm_compute in 1 +' "3a". (* ==> "a" : string, à la manière du C *)

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

L'analyse polyédrique a été proposée pour l'optimisation et la parallélisation en compilation depuis la fin des années 80

Cela confirme une partie de la discussion qui suit la conférence : il semblerait que ce soit le bug d'Ariane V qui ait amené à s'intéresser à ce genre de technique.

Je ne me suis jamais penché sur la complexité de ce type d'algorithme, mais j'ai une question sur deux de tes remarques :

Mais utiliser un solveur ILP mène à de sérieuses contraintes, entre autres que le temps de résolution des (in)équations augmente exponentiellement avec la complexité du nid de boucle à paralléliser/optimiser.

et

Bref. Pour passer d'un modèle mathématique correct, et qui fonctionne sur des programmes/boucles jouet, à un compilateur qui peut compiler du « vrai » code (principalement scientifique), il a fallu attendre environ 20 ans (et sacrifier pas mal de thésards à l'autel du modèle polyédrique).

Les cas pathologiques pour la complexité exponentielle, on les rencontres dans du « vrai » code ? Je pose la question parce que, pour revenir sur le thème du journal et les ADT, ce système de type et son mécanisme d'inférence est basé sur l'algorithme d'unification de Robinson (milieu des années 1960) et le système Hindley-Milner ou le système F (début des années 70). Pour l'étude de la compléxité, il a fallu attendre 1991 et elle est doublement exponentielle. Xavier Leroy en propose une étude dans son livre sur le langage Caml (page 360 du livre et 370 du pdf). Cela étant, dans la « vraie » vie, sur du « vrai » code, on observe que l'algorithme se comporte linéairement : quand on double la taille du programme, on double le temps de compilation. Les pires cas en compléxité temporelle sont pathologiques; et à mon avis un programmeur qui les écriraient auraient soit l'esprit totalement tordu, soit aurait le cerveau qui exploserait bien avant de faire chauffer son CPU pour essayer de comprendre son propre code.

P.S : pour la vidéo, je les regarde en streaming via le lecteur proposé sur la page en question. Mais plus que la présentation des différentes techniques d'analyse statique, ce que je trouve intéressant c'est la discussion avec le public qui suit la présentation.

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

Oui, c'est bien la méthode B et l'atelier B qui est derrière tout ça. C'est un successeur du formalisme Z qui a inspiré le langage Eiffel et sa programmation par contrat.

Son inventeur, Jean-Raymond Abrial, est revenu sur l'histoire de ces approches dans une conférence au Collège de France dont voici la présentation :

Cette présentation est celle d’un chercheur vieillissant qui porte un regard historique sur les trente dernières années de son travail.

Il y a deux sortes de chercheurs : les prolifiques et les monomaniaques. Je fais partie de la seconde catégorie, car j'ai toujours pratiqué le même genre d’investigations, à savoir la spécification et la construction vérifiée de systèmes informatisés.

Ce travail, autant théorique que pratique, s’est concrétisé au cours de toutes ces années dans trois formalismes voisins : Z, B et Event-B (dont je ne suis pas, loin de là, le seul contributeur). Je vais tenter d’expliciter comment les idées que contiennent ces formalismes et les outils correspondants ont lentement émergés de façon parfois erratique.

Je tenterai aussi de préciser les multiples influences qui ont participé à cette évolution. En particulier, je montrerai comment plusieurs réalisations industrielles ont permis de progresser dans ce domaine. Mais je soulignerai aussi les échecs et parfois les rejets de la part de communautés tant universitaires qu’industrielles.

Pour finir, je proposerai quelques réflexions et approches pour le financement de recherches telles que celle-ci.

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

Sur un simple enregistrement variant, l'information n'est pas portée avec le type dans la signature d'une fonction. Je peux comprendre qu'on puisse préférer que le compilateur refuse tout simplement de compiler lorsque la vérification est hors de portée.

Si la vérification est hors de portée du compilateur (avec une pleine certitude), alors il ne doit pas refuser de compiler (tout au plus, peut-il émettre un avertissement pour signaler ce qu'il ne peut savoir au cas où cela pourrait poser un problème au développeur) mais prendre des précautions en plaçant un test à l'exécution (ce qui semble être le cas).

J'ai réfléchi, depuis, à cet exemple en ADA et l'impossibilité pour le compilateur de suivre le bon typage d'une telle valeur vient peut être de sa mutabilité. Dans ton exemple, on voit bien qu'il y a là un problème. Mais, de ce que j'ai compris, cette variable pourrait se voir attribuer une valeur connue dynamiquement (après calcul d'une fonction par exemple) qui serait du bon type et possédant, cette fois, le champ en question.

Avec les ADT (même avec des valeurs mutables, comme en OCaml) ce n'est pas possible, car l'existence du champ est marquée par le constructeur de type qu'il faut nécessairement déconstruire.

type politique =
  | NbreFixe of int
  | NbreMaxHardware
  | PasDeThreading
  | CasParticulier;;

(* ici le terme est une variable mutable *)
let ma_politique = ref CasParticulier;;
let _ = ma_politique := NbreFixe 3;;

let i = match !ma_politique with
  | NbreFixe n -> n
  | _ -> assert false
val i : int = 3

Oups, désolé, je ne sais plus comment on a réussi à dériver d'une discussion qui par du compilateur Haskell pour finir par parler des langages objets. Toute mes excuses pour des propos qui auraient pu être interprétés comme blasphématoires dans ce fil de discussion de conviction plutôt fonctionnelle.

Il n'y a rien de blasphématoires dans ce fil, c'est toujours intéressant de voir comment une problématique peut être abordée dans d'autres langages et paradigmes. Et comme je l'avais signalé dans la dépêche sur le compilateur 4.03 de OCaml, c'est du code ADA qui fait tourner les lignes automatiques du métro parisien ;-) (même s'il n'a pas été écrit à la main, mais généré à partir d'un langage plus haut niveau).

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

Désolé si mon message a pu paraître agressif, telle n'était pas mon intention. C'est juste que je ne voyais pas où tu voulais en venir, ni le rapport avec les discussions du journal et des commentaires qu'il a suscités. Ma réaction était du même ordre que la fameuse réplique :

-- il dit qu'il a plus de genoux
-- il dit qu'il voit pas le rapport.

L'exemple central du journal tourne autour des garanties statiques que peut apporter Haskell (ou plus généralement, le système des ADT) pour la conception d'API et éviter les erreurs à l'exécution. S'en est suivi différentes discussions, avec des illustrations en ADA, Haskell ou OCaml, qui tournent toutes autour de ce même thème : peut-on (et si oui comment ?) contrôler la bonne formation des termes à la compilation (statiquement), ou doit-on mettre des gardes-fous et des tests lors de l'exécution (dynamiquement) ?

Ainsi lorsque je parlais d'outils d'analyses statiques, je ne considérais que ceux dont l'objectif se situe dans la gestion de cette problématique. C'est pour cela qu'à chacune de mes réponses, j'ai rappelé le contexte de la discussion. Je ne sous-entendais pas que les outils d'analyses de code se limitaient à gérer cette question. Et pour tous les cas d'usages que tu mentionnes, cela n'aurait d'ailleurs aucun sens d'avoir une alternative pour les traiter dynamiquement.

Une petite précision pour conclure :

Comme tu dis régulièrement que tu n'es pas développeur et que tu ne connais pas « l'industrie » ça ne me surprenait pas que tu ne connaisse pas ce pan là.

Il est vrai que je ne suis pas développeur (bien que je saches programmer, mais c'est loin d'être ma préoccupation première), et que je ne connais pas l'industrie. Mais quand je dis cela, c'est surtout pour exprimer que je ne sais pas ce qui est passé des laboratoires de recherche (et qui y est notoirement connu) vers le domaine industriel, ni le vocabulaire associé et le changement de dénomination qu'ont pu subir les notions lors du passage (ce qui est aussi parfois le cas lorsque la notion passe du domaine des mathématiques pures et de la logique à celui de l'informatique théorique).

Si je prends un exemple pour illustrer la chose. Dans la vidéo de la conférence sur JML (dont le lien était erroné, le voici), l'orateur expose sur un cas particulier une méthode d'analyse statique dite analyse polyédrique (vers la 40ème minute). Il conclue l'étude de cette exemple avec une diapo qui contient ce passage :

Principe de l'analyse de programme :

• traduction vers un flux d'équation sur des ordres partiels
• résolveur général basé sur des itérations

et la méthode de résolution (comme il le souligne à l'oral) est en partie fondée sur des travaux de Tarski qui datent des années 1930. Résultats auxquels j'avais fait allusion dans un autre journal. Ce type de technique se retrouve dans les solveurs SMT (Satisfiability modulo theories), comme par exemple l'outil alt-ergo (écrit en OCaml) utilisé, entre autre, par Spark dont a parlé Blackknight.

Les résultats de Tarski me sont connus depuis une bonne quinzaine d'années (époque où j'étais étudiant), et ce genre de conférence me permet de savoir que des industriels peuvent en faire usage (quant bien même ils ignoreraient ce qui se trouve sous le capot, ou dans quel contexte et pour quelles raisons ces problèmes ont été résolus à une époque où l'ordinateur n'existait pas encore).

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

Dans le cas de l'attribut qui n'existe pas selon le discriminant, il n'y aura même pas de Waring à la compilation. Uniquement une Erreur au Runtime. Ça me semble difficile de détecter tous les mauvais usages d'un type variant, surtout si on peut récupérer le record depuis un contexte extérieur (non-Ada). Il faut bien que ça plante quelque part, au niveau de l'interface, si on fait de la programmation par contrat, ou plus loin dans le code si on ne teste pas à l'entrée.

Dans le cas où le code produit peut être utilisé via un autre langage qui ne permettrait pas de détecter statiquement l'erreur, assurément il faut bien alors mettre en place un contrôle dynamique avec émission d'une erreur. Cela relève du principe élémentaire dans le domaine réseau : « be conservative in what you send, be liberal in what you receive ». Ne sachant pas, a priori, ce que le code peut recevoir en entrée, il faut s'attendre à tout et être capable de gérer une erreur à l'exécution. Mais dans ton cas, le code est utilisé dans un contexte ADA et l'erreur est repérable statiquement. Détecter, dans ce cas, tous les mauvais usage d'un type variant à la compilation n'est pas une chose difficile : c'est le principe même du type checking, tâche qui incombe au compilateur dans les langages à typage statique.

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

Et justement, je dis que les analyseurs statiques servent aussi à refuser du code qui fonctionne parfaitement, mais qui ne correspond pas aux normes défini dans le programme en question par exemple.

Soit mais là on est un plus dans un problème de définition de terme : je ne dispute jamais des mots pourvu que l'on me dise le sens qu'on leur donne.

Mon commentaire était en réponse à un échange entre Guillaum et gerfaut83 au sujet d'un bout de code ADA et du comportement du compilateur. Guillaum s'étonnait de l'absence de garantie statique (absence d'erreur de typage à la compilation), ce à quoi gerfaut83 lui a répondu qu'on se trouvait à la limite entre le travail du compilateur et celui d'un analyseur statique.

Je réponds alors : le type checking (tache qui incombe au compilateur) c'est de l'analyse statique; et dans l'exemple donné il y a clairement un problème de typage qui peut être détecté statiquement, c'est-à-dire à la compilation. Puis j'illustre mon propos sur un exemple pour montrer en quoi cela peut être utile : réduire l'overhead à l'exécution. Comme la chose est vérifiée une bonne fois pour toute à la compilation, il n'est pas nécessaire de faire un test dynamiquement qui générera une exception.

Ensuite, répondre que l'on peut faire rentrer dans la catégorie des tâches dévolues à l'analyse statique d'autres problématiques que le contrôle d'erreurs est hors de propos. Généraliser le concept de l'analyse statique au-delà du cas d'étude ici discuté fait de ton objection une sorte de stratagème III : la généralisation des arguments adeverses :

Il s’agit de prendre une proposition κατα τι, relative, et de la poser comme απλως, absolue ou du moins la prendre dans un contexte complètement différent et puis la réfuter. L’exemple d’Aristote est le suivant : le Maure est noir, mais ses dents sont blanches, il est donc noir et blanc en même temps. Il s’agit d’un exemple inventé dont le sophisme ne trompera personne. Il faut donc prendre un exemple réel.

Exemple 1

Lors d’une discussion concernant la philosophie, j’ai admis que mon système soutenait les Quiétistes et les louait. Peu après, la conversation dévia sur Hegel et j’ai maintenu que ses écrits étaient pour la plupart ridicules, ou du moins, qu’il y avait de nombreux passages où l’auteur écrivait des mots en laissant au lecteur le soin de deviner leur signification. Mon adversaire ne tenta pas de réfuter cette affirmation ad rem, mais se contenta de l’argumentum ad hominem en me disant que je faisais la louange des Quiétistes alors que ceux-ci avaient également écrit de nombreuses bêtises.

J’ai admis ce fait, mais pour le reprendre, j’ai dit que ce n’était pas en tant que philosophes et écrivains que je louais les Quiétistes, c’est-à-dire de leurs réalisations dans le domaine de la théorie, mais en tant qu’hommes et pour leur conduite dans le domaine pratique, alors que dans le cas d’Hegel, nous parlions des ses théories. Ainsi ai-je paré l’attaque.

Les trois premiers stratagèmes sont apparentés : ils ont en commun le fait que l’on attaque quelque chose de différent que ce qui a été affirmé. Ce serait un ignoratio elenchi de se faire battre de telle façon. Dans tous les exemples que j’ai donnés, ce que dit l’adversaire est vrai et il se tient c’est en opposition apparente et non réelle avec la thèse. Tout ce que nous avons à faire pour parer ce genre d’attaque est de nier la validité du syllogisme, c’est-à-dire la conclusion qu’il tire, parce qu’il est en tort et nous sommes dans le vrai. Il s’agit donc d’une réfutation directe de la réfutation per negationem consequentiæ.

Il ne faut pas admettre les véritables prémisses car on peut alors deviner les conclusions. Il existe cependant deux façons de s’opposer à cette stratégie que nous verrons dans les sections 4 et 5.

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

Toutes les discussions que l'on voit au dessus montrent justement qu'il y a suffisamment de façon de résoudre un problème pour que ça ne soit pas figé dans le langage. Pour autant tu peux vouloir, au sein d'un programme donné, n'autoriser qu'une seule solution à fin d'améliorer la cohérence.

Où vois-tu dans mon propos que c'est figé dans le langage ? La discussion portait sur un bout de code ADA, celui-ci :

MaPolitique := (Politique => CasParticulier);
MaPolitique.NombreThread := 5; -- CONSTRAINT_ERROR : discriminant check failed

qui générera une exception à l'éxecution car, dans ce cas du variant, il n'y a pas de champ NombreThread. C'est là une problématique de typage, et d'ailleurs le compilateur semble savoir qu'il y a problème, mais la norme semble avoir préférée émettre un warning et non une erreur de compilation. D'où la question de Guillaum : « Il n'y a pas de garantie statique sur ce genre de chose ? Ça c'est dommage ». Question à laquelle gerfaut83 a répondu : « J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code ».

D'une manière générale, le principe du typage statique se situe dans la question : comment refuser d'exécuter un code qui plantera nécessairement ? ou plutôt, comment savoir qu'un bout de code plantera nécessairement avant de le lancer ? D'où mon exemple pour refuser statiquement, par contrainte de type, un arbre vide comme entrée pour une fonction plutôt que de générer une exception à l'exécution; solution qui de plus réduit l'overhead du code généré.

Dans l'exemple ci-dessus, ce n'est pas tant une impossibilité d'inférer statiquement qu'il y aura un problème, mais un choix de la norme qui considère cela comme un avertissement et non comme une erreur critique. Mais dans bien des cas, sans ajout d'informations qui ne sont pas définies par le langage, il n'est pas possible de garantir certains invariants d'un code. Ce à quoi je faisais référence, pour aborder cette problématique, était des outils d'analyse statique comme JML pour Java présenté, par exemple, dans la conférence Intégration de la vérification formelle dans les langages de programmation.

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

J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code.

Certes, mais le contrôle de type (type checking) effectué par un compilateur relève de l'analyse statique de code. Dans les faits, on ajoute des outils d'analyse statique de code à l'extérieur du compilateur pour pallier aux déficiences du système de types d'un langage. Et pour fonctionner, ces outils nécessitent habituellement l'ajout d'annotations au code sous forme de commentaires, annotations qui correspondent à un enrichissement du langage des types du langage de départ.

Dans tout langage de programmation, il y a en réalité deux langages :

• le langage des termes pour décrire les calculs à effectuer ;
• le langage des types pour rejeter à la compilation, ou à l'exécution, certains termes comme sémantiquement invalides (vides de sens).

Plus le langage des types est évolué, plus il permet de contrôler la bonne formation des termes à la compilation (c'est-à-dire statiquement). L'idée des ADT est de pouvoir effectuer du raisonnement par cas non sur la valeur des termes (ce qui ne peut se faire qu'à l'exécution, là où la valeur est connue) mais sur leur type (ce qui est connu statiquement à la compilation).

On peut même pousser le principe plus loin avec des GADT pour discriminer plus fortement la construction des termes, et faciliter l'optimisation du code généré sans avoir à gérer d'exception au runtime. Je vais l'illustrer sur un exemple en OCaml avec une fonction qui retourne la valeur du nœud racine d'un arbre binaire parfait.

Avec les ADT, on peut encoder les arbres binaires parfaits ainsi :

type 'a t =
  | Empty : 'a t
  | Node : 'a * ('a * 'a) t -> 'a t

Les contraintes sur le type ne permettent que de construire des arbres parfaits : soit l'arbre est vide, soit c'est un nœud qui contient une valeur de type a et un arbre paramétré par un couple de type 'a * 'a (ce qui représente les sous-arbres gauche et droite).

Pour extraire, la valeur du nœud racine on procède ainsi :

let top = function
  | Empty -> failwith "Empty tree"
  | Tree (v, _) -> v

La fonction retournera une exception à l'exécution si on lui passe un arbre vide :

top Empty;;
Exception: Failure "Empty tree".

Maintenant, avec les GADT, on peut encoder ce type d'arbre ainsi :

type z = Z
type 'n s = S : 'n -> 'n s

type ('a, 'n) t =
  | Empty : ('a, z) t
  | Tree : ('a, 'n) t * 'a * ('a, 'n) t -> ('a, 'n s) t

Ici, c'est plus subtil et plus précis au niveau des contraintes de types. On commence par encoder les entiers dans le système de type avec z pour représenter zéro, et 'n s pour représenter la fonction successeur. Ensuite, on paramètre le type des arbres à la fois par le type des nœuds ('a) ainsi que par sa profondeur ('n). La définition dit qu'un arbre vide est de profondeur nulle et que les sous-arbres d'un nœud ont la même profondeur 'n (l'arbre est parfait) et que sa profondeur est 'n + 1 = 'n s.

Pour coder la fonction top, il est n'est plus nécessaire de traiter le cas de l'arbre vide :

let top : type a n. (a, n s) t -> a = function
  | Tree (_, v, _) -> v

Le type de la fonction déclare explicitement que la profondeur de l'arbre est du type successeur ('n s) et donc l'arbre ne peut être vide. Cette fois, si on lui passe un arbre vide, on a une erreur de typage à la compilation :

top Empty;;
Error: This expression has type ('a, z) t
       but an expression was expected of type ('a, 'b s) t
       Type z is not compatible with type 'b s

Pour ce qui est du code généré par le compilateur (option -dlambda du compilateur), on peut vérifier qu'il peut faire l'économie d'un test à l'exécution.

Avec ADT, on obtient :

let 
  (top =
    (function p
      (if p (field 0 p)
        (apply (field 1 (global Pervasives!)) "Empty tree"))))

Avec les GADT, on a :

let (top = (function p (field 1 p))

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