Je recopie ici le passage d'une de mes commentaires dans un des ces journaux :
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.
Le résultat est intéressant en lui même, ne serait-ce que pour légitimer l'autorité du président élu, mais si quelqu'un a des sources plus précises et exactes, je suis intéressé.
Sans vouloir nier la véracité des faits rapportés par Nicolas Grégoire, on ne peut pas dire qu'en dehors de sa parole il apporte la moindre preuve via ses documents (comme la fort bien souligné Michaël dans son commentaire).
Mais dans le fond, c'est une pratique courante et répandue dans tous les partis cet usage des assistants parlementaires. Sans vouloir en prendre la défense, ni minimiser de tels abus, je suis étonné par une certaine candeur de la population face aux « révélations » de ce genre de faits.
Enfin, si la volonté était de pointer du doigt Macron, il n'était pas nécessaire de remonter si loin dans le temps en passant par une attaque contre Bayrou. L'emploi parlementaire sur mesure du fondateur des Jeunes avec Macron ou comment bosser deux jours par semaine pour plus de 3000€ et pouvoir consacrer le reste de son temps « bénévolement » pour la campagne de Macron.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
De rien. Vu que tu n'avais jamais utilisé les backports, tu peux lancer un :
apt-get -t jessie-backports upgrade
pour voir tous les paquets que tu peux mettre à jour dans leur version backportée. Et si tu veux aller plus loin, mais c'est plus risqué et tendu, tu peux jouer avec le apt pinning.
Ou en plus secure, mais plus long en temps de calcul (cela lance un solveur SAT pour vérifier si le paquet est installable en gérant les conflits entre paquets) :
apt-get install apt-cudf aspcud
puis pour installer un paquet :
apt-get --solver aspcud install ton-paquet
Il y a quelques articles d'exemples sur le blog de Roberto DiCosmo. Cette méthode permet d'installer des paquets que le solveur interne de apt-get aurait refusé pour cause de conflits.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Oui c'est normal. Debian ne met pas ses versions à jour au cours d'une version stable mais effectue seulement des correctifs de sécurité. Ubuntu n'est pas basé sur la version stable de Debian. Raspbian recompile et patch les paquets sources Debian et a son propre noyau pour l'adapter aux spécificités du matériel.
Disons que c'est bien ce que laissait sous-entendre l'auteur du journal qui soit n'avait pas lui-même compris la situation, soit a fait preuve de malhonnêteté intellectuelle.
Cela étant, je ne suis pas certain que ce document à lui seul ait permis de pouvoir voter. Il fait bien mention d'une application de l'article L. 34, mais il est signé par le maire de l'arrondissement. Or, d'après l'article en question, seul le juge de tribunal d'instance peut statuer. Il se peut, comme l'indique le titre du papier, que le maire atteste simplement de l'existence d'une erreur matérielle et qu'il faille ensuite, muni du document, saisir le juge pour obtenir définitivement l'inscription.
Quoi qu'il en soit, un système infaillible est quasi-impossible à mettre en place, mais le notre est fait de telle sorte qu'il soit possible de corriger ses « bugs » si l'on s'en rend compte à temps.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
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.
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.
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.
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.
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.
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 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 *)Inductivenat:=|O:nat|S:nat->nat.Fixpointplusnm:=matchnwith|O=>m|Sp=>S(pluspm)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 *)Theoremplus_assoc:forallnmp,n+m+p=n+(m+p).Proof.inductionn.-simpl.trivial.-simpl.intros.rewriteIHn.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 :
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 :
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 :
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 :
Check1+'"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 :
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. *)InstanceStr_append:monoidappend"".Proof.split.-inductionx;[auto|intros;simpl;rewriteIHx;reflexivity].-reflexivity.-inductionx;[auto|simpl;rewriteIHx;reflexivity].Qed.(* maintenant on vérifie le type et on évalue : *)Check"1"+'"3a".(* ==>"1" +' "3a" : string *)Evalcomputein"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.
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 :
Evalcomputein1+'"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. *)Evalvm_computein1+'"3a".(* ==>Error: vm_compute does not support existential variables. *)Instancenat_add:bin_opnatnatnat:={op:=plus}.Instancestr_app:bin_opstringstringstring:={op:=append}.Instancenat_str:bin_opnatstringstring:={opns:=matchgetnswith|None=>""|Somec=>Stringc""end}.Evalvm_computein1+'3.(* ==> 4 : nat *)Evalvm_computein"1"+'"3a".(* ==> "13a" : string *)Evalvm_computein1+'"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.
[^] # Re: Abstention abstention ...
Posté par kantien . En réponse au journal Résultats des elections, qui est le vrai vainqueur ?. Évalué à 6. Dernière modification le 08 mai 2017 à 23:06.
Aucun système n'est parfait mais le notre est un des pires que l'on puisse concevoir.
Ce n'est pas comme si le sujet était inconnu et non documenté :
ni que certains journaux avaient évoqué le sujet dernièrement :
Bonne lecture. :-)
Je recopie ici le passage d'une de mes commentaires dans un des ces journaux :
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Résultats
Posté par kantien . En réponse au journal Résultats des elections, qui est le vrai vainqueur ?. Évalué à 10.
Le flegme est un trait de caractère typiquement britannique, à ne pas confondre avec la flemme.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
# Source officielle
Posté par kantien . En réponse au journal Résultats des elections, qui est le vrai vainqueur ?. Évalué à 10.
Oui, les résultats officiels sur le site du ministère de l'intérieur.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
# Pourquoi remonter si loin dans le temps ?
Posté par kantien . En réponse au journal Les langues se délient.... Évalué à 6.
Sans vouloir nier la véracité des faits rapportés par Nicolas Grégoire, on ne peut pas dire qu'en dehors de sa parole il apporte la moindre preuve via ses documents (comme la fort bien souligné Michaël dans son commentaire).
Mais dans le fond, c'est une pratique courante et répandue dans tous les partis cet usage des assistants parlementaires. Sans vouloir en prendre la défense, ni minimiser de tels abus, je suis étonné par une certaine candeur de la population face aux « révélations » de ce genre de faits.
Enfin, si la volonté était de pointer du doigt Macron, il n'était pas nécessaire de remonter si loin dans le temps en passant par une attaque contre Bayrou. L'emploi parlementaire sur mesure du fondateur des Jeunes avec Macron ou comment bosser deux jours par semaine pour plus de 3000€ et pouvoir consacrer le reste de son temps « bénévolement » pour la campagne de Macron.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: 4.11
Posté par kantien . En réponse à la dépêche Sortie du noyau Linux 4.10. Évalué à 4.
De rien. Vu que tu n'avais jamais utilisé les backports, tu peux lancer un :
pour voir tous les paquets que tu peux mettre à jour dans leur version backportée. Et si tu veux aller plus loin, mais c'est plus risqué et tendu, tu peux jouer avec le apt pinning.
Ou en plus secure, mais plus long en temps de calcul (cela lance un solveur SAT pour vérifier si le paquet est installable en gérant les conflits entre paquets) :
puis pour installer un paquet :
Il y a quelques articles d'exemples sur le blog de Roberto DiCosmo. Cette méthode permet d'installer des paquets que le solveur interne de
apt-getaurait refusé pour cause de conflits.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: 4.11
Posté par kantien . En réponse à la dépêche Sortie du noyau Linux 4.10. Évalué à 5.
Oui, il faut bien ajouter le dépôt backports à ton
sources.listpuis cibler celui-ci lors d'une commande d'installation de paquet :Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: 4.11
Posté par kantien . En réponse à la dépêche Sortie du noyau Linux 4.10. Évalué à 9. Dernière modification le 02 mai 2017 à 22:46.
Oui c'est normal. Debian ne met pas ses versions à jour au cours d'une version stable mais effectue seulement des correctifs de sécurité. Ubuntu n'est pas basé sur la version stable de Debian. Raspbian recompile et patch les paquets sources Debian et a son propre noyau pour l'adapter aux spécificités du matériel.
Pour avoir un noyau 4.9 avec Jessie, il faut utiliser les backports.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Tu vas vites en besogne
Posté par kantien . En réponse au journal Et si les "erreurs purement matérielles" pouvaient influer sur le processus démocratique. Évalué à 2. Dernière modification le 30 avril 2017 à 10:17.
Disons que c'est bien ce que laissait sous-entendre l'auteur du journal qui soit n'avait pas lui-même compris la situation, soit a fait preuve de malhonnêteté intellectuelle.
Cela étant, je ne suis pas certain que ce document à lui seul ait permis de pouvoir voter. Il fait bien mention d'une application de l'article L. 34, mais il est signé par le maire de l'arrondissement. Or, d'après l'article en question, seul le juge de tribunal d'instance peut statuer. Il se peut, comme l'indique le titre du papier, que le maire atteste simplement de l'existence d'une erreur matérielle et qu'il faille ensuite, muni du document, saisir le juge pour obtenir définitivement l'inscription.
Quoi qu'il en soit, un système infaillible est quasi-impossible à mettre en place, mais le notre est fait de telle sorte qu'il soit possible de corriger ses « bugs » si l'on s'en rend compte à temps.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Tu vas vites en besogne
Posté par kantien . En réponse au journal Et si les "erreurs purement matérielles" pouvaient influer sur le processus démocratique. Évalué à 5.
Ç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.
Ou encore :
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…
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.
[^] # Re: Libre, pas libre, c'est douteux
Posté par kantien . En réponse au journal grsecurity abandonne le gratuit. Évalué à 4. Dernière modification le 28 avril 2017 à 11:52.
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.
[^] # Re: Referers
Posté par kantien . En réponse au journal Expérimentation "Voter Autrement : Présidentielles 2017". Évalué à 7. Dernière modification le 22 avril 2017 à 18:17.
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.
[^] # Re: Coquille
Posté par kantien . En réponse à la dépêche Résultat électoral : le nouveau DPL est…. Évalué à 4.
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 ! :-PSapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Merci pour la dépêche
Posté par kantien . En réponse à la dépêche Rudder 4 — nouvelle version de la solution de Continuous Configuration. Évalué à 6.
Elle l'est, c'est écrit dans la dépêche à la section ergonomie de l'interface web :
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Modes de scrutins
Posté par kantien . En réponse à la dépêche Résultat électoral : le nouveau DPL est…. Évalué à 4.
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.
[^] # Re: Modes de scrutins
Posté par kantien . En réponse à la dépêche Résultat électoral : le nouveau DPL est…. Évalué à 10.
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.
[^] # Re: Modes de scrutins
Posté par kantien . En réponse à la dépêche Résultat électoral : le nouveau DPL est…. Évalué à 2.
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.
[^] # Re: Réponse de Acer confirmant le remboursement de MS-Windows mais avec l'envoi du PC
Posté par kantien . En réponse au journal Comparatif des prix des hybrides portable/tablette et remboursement MS-Windows. Évalué à 4.
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.
[^] # Re: Méthode de Condorcet
Posté par kantien . En réponse au journal Résultat électoral : le nouveau DPL est.... Évalué à 9. Dernière modification le 19 avril 2017 à 11:39.
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.
[^] # Re: Machine a dépouillé
Posté par kantien . En réponse au journal Vote à l'urne et vote électronique. Évalué à 5. Dernière modification le 18 avril 2017 à 14:01.
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.
[^] # Re: et le bilan ?
Posté par kantien . En réponse au journal Résultat électoral : le nouveau DPL est.... Évalué à 6.
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.
# Coquille sur le nom d'un des candidats.
Posté par kantien . En réponse au journal Résultat électoral : le nouveau DPL est.... Évalué à 4.
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.
[^] # Re: J'aime bien l'idée !
Posté par kantien . En réponse au journal Jugement majoritaire. Évalué à 8.
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.
[^] # Re: Wow
Posté par kantien . En réponse au journal Macron, ou la destruction du pouvoir législatif. Évalué à -3.
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.
[^] # Re: Un peu déçu par Rust
Posté par kantien . En réponse au journal Un print(1 + "3a"), ça nous inspire comment ?. Évalué à 3.
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 :
Les preuves en Coq ou Idris peuvent se paraphraser ainsi :
On prouve le théorème par récurrence sur l'entier
n.n = 0alors après simplification il faut prouver quem + p = m + pce qui est trivial.n = S n'alors il faut montrerS n' + m + p = S n' + (m + p), ce qui revient, par définition de la fonctionplus, à montrer queS (n' + m + p) = S (n' + (m + p))(c'est là l'appel à la tactiquesimplqui effectue des réductions de calcul à partir de la définition deplus). Or, d'après l'hypothèse de récurrence on an' + m + p = n' + (m + p), il suffit donc de montrerS (n' + (m + p)) = S (n' + (m + p))(là c'est la sérieintros. 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 :
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 :
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 :
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.
[^] # Re: Un peu déçu par Rust
Posté par kantien . En réponse au journal Un print(1 + "3a"), ça nous inspire comment ?. Évalué à 5.
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 + yque dans une structure de monoïde. Alors je vais le faire façon type classes à la Haskell :Là on fait un type checking sur la fonction
monoid_op:Elle prend deux valeurs d'un certain type
?Aet 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 valeurAtelle que …). Si on lui demande de typer l'expression1 +' "3a", on obtient :Mais le plus amusant est qu'il peut typer le terme
"1" +' "3a"avant même de savoir le calculer :Maintenant pour lui permettre de calculer, on lui fournit une instance de la classe :
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.
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 :
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.