Michaël a écrit 2935 commentaires

Merci pour tes slides, dont j'aime bien le ton et le contenu! Tout naïf que je suis je n'avais pas fait explicitement le rapprochement entre l'isomorphisme de Curry-Howard et la logique intuitionniste. :) Je vais donc t'obliger à faire le SAV. :D

La façon de comprendre la traduction entre de “truth” et “falsity” en termes de CS “type singleton” et “type vide” est que “A implique B est vraie” et “il existe une et une seule fonction de A vers B”, correct?

Est-ce qu'il n'y a pas un poly que tu pourrais me recommander. Je suis mathématicien mais je ne suis pas très familier avec le domaine de la logique proprement dite ou la théorie des types, donc je pense que je pourrais arriver à profiter un peu d'un cours de DEA ou de Master.

S'il n'est pas liquide, ça le disqualifie totalement comme monnaie!

à partir du moment ou des gens utilisent le bitcoin comme représentation arbitraire de valeur, c'est une "vraie" monnaie.

Tu constates que le bitcoin a un marché relativement liquide, on peut trouver des gens prêt à échanger du bitcoin contre d'autres choses. Mais ça n'en fait pas une vraie monnaie (qui n'a pas besoin de guillemets) autour du mots vrai. Il y a des tas de choses qui, comme le bitcoin, ont des marchés liquides et n'ont pas de contrepartie physique, comme beaucoup de produits dérivés – les options par exemple. Mais ça ne fait pas des options ou des autres produits dérivés une monnaie. La garantie apportée par un pouvoir politique est une des caractéristiques les plus importantes de monnaies.

Je suis sensé bientôt faire un exposé sur OCaml devant le Rust USer Groups de Cologne, mais c'est pas encore tout à fait officeil :D

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.

Dans quel types de contexte est-ce que coq est utilisé. J'avais lu des articles concernant des utilisations dans les transactions bancaires, il s'agissait d'un exemple essentiellement académique sur un très petit sous-système. Du coup je n'ai pas trop d'intuition sur la taille des programmes qu'on peut pratiquement prouver avec coq. Est-il facile de travailler sur les appels-système, comme par exemple pour démontrer dans un programme que toutes les conditions d'erreur sont correctement traitées?

Est-ce que tu sais ce que devient focal?

Enfin, je ne suis pas logicien, mais mathématicien, du coup j'ai essayé de me mettre dans la peau do coq. La première seconde, je me suis dit, “hey chouette:”

Il existe x tel que P <-> Il existe un programme calculant x tel que P

par contre pour transformer le pour tout en logique intuitionniste, j'ai moins fait le malin puisque la formulation

pour tout x on a P <-> Non(Il existe x tel que Non P) <-> Il n'existe aucun programme calculant x tel que non P

me paraît préparer beaucoup de problème à celui qui voudrait s'en servir. :) Du coup que font les intuitionnistes pour traduire les énoncés en “pour tout”? Est-ce que c'est ce “second ordre” que j'ai jusqu'ici négligé qui sauve les meubles? Ou bien est-ce qu'ils se lancent dans des considérations énumératives?

Ah j'habite à Bonn / Cologne :)

Très bien merci!

Sehr schön, danke! :)

Si j'ai bien compris, tu travailles à Lille? Vous avez des bureaux en Allemagne?

Je suis parfaitement d'accord avec toi, l'apport des langage fonctionnels touche surtout à la garantie qu'un code qui compile sera un code qui fonctionne (sauf erreur de conception).

Exactement, dans ma pratique quotidienne, les seules erreurs qui échappent au compilateur sont “les miennes” i.e. les erreurs intelligentes – mauvais algorithme, mauvais emploi des ressources système – que tu appelles erreurs de conception.

Sérieusement, une interface ne se limite pas aux signatures de fonctions… La sémantique, c'est pour les chiens ?

Il grossit un peu le trait, mais un des charmes des langages comme OCaml est qu'ils sont très expressifs – donc on a à sa disposition un vocabulaire de haut niveau – et que le système de types est une information supplémentaire sur le programme. Cette information permet au compilateur de détecter des erreurs, mais le programmeur a aussi un degré de liberté supplémentaire, et on peut représenter des invariants importants du programme dans le système de type (du genre, connection initialisée) ce qui permet d'utiliser le compilateur comme un système de preuve correction allégé. Je précise que OCaml n'a pas de RTTI (on dit que les types sont effacés à la compilation) et que ceci n'a donc aucune surcharge au “runtime”.

Ensuite mon expérience est que lorsque je programme je fais surtout des erreurs d'étourderie et presque jamais des erreurs de sémantique – les premières sont presque toutes capturées par le compilateur et les autres, c'est le boulot de la test-suite.

sans vouloir jouer les rabats-joie tout le monde (ou presque) expose une API REST.

En plus en utilisant webmachine et yojson c'est du pipi de chat!

Sinon c'est pas super tendance, les RPCs existent depuis le début des années 80. Ce qui est nouveau, c'est que HTTP/JSON s'est plus ou moins établi en standard de fait depuis quelques années.

Oui merci de réparer cet oubli, l'apport de OCamlPro est très important et très stimulant pour la communauté!

Après je suis pas sur que l'INRIA développe toujours sur OCaml. Est-ce qu'ils sont des projets en OCaml?

Si tu t'intéresses à OCaml il faut savoir que la communauté OCaml connaît depuis deux ans une sorte de printemps, notamment grâce à la publication de opam — un gestionnaire de paquets pour OCaml — qui permet très facilement de profiter du code des autres.

OCaml est utilisé par plusieurs industries en France et dans le monde, le consortium compte notamment des poids lourds comme Dassault, Microsoft ou Bloomberg. OCaml est un langage très polyvalent, qu'on peut utiliser pour la modélisation des risques financiers (JaneStreet, Lexifi), les preuves formelles (Coq, utilisé en milieu industriel) ou la programmation système (je l'utilise pour mes travaux de DevOps). Sur ce dernier point tu peux jeter un coup d'œil à mon GitHub puisque mon employeur me permet de libérer une partie du code que nous utilisons. Ensuite, un petit tour sur la liste “awseome OCaml” sur GitHub, le reddit, ou la mailing list (uncoOol? mais non! ☺) devrait te convaincre que le langage se porte très bien et est plein de perspectives intéressantes.

Je ne connais pas trop Haskell, mais je sais qu'il est utilisé par HSBC pour faire de la gestion de risque financier.

Et puis on voit bien que les distributions ressemblent plus à des lois log-normales que des normales. À moins qu'il ne s'agisse d'une des nombreuses autres distribution qui ont un profil similaire. :)

Ta proposition que chacun reparte dans son coin avec sa vérité ne me semble pas des plus intéressantes. Afficher l'ensemble des points de vues, discuter, argumenter, sourcer sur le long terme me semble le plus pertinent. Et wikipedia est très bien pour ça

Je suis complètement d'accord avec toi – et pas seulement sur la partie que je cite. Cependant c'est un des défauts de Wikipédia de présenter un aspect trop lisse qui a un côté “tables de la loi”. Ce serait intéressant que la partie rédaction et critique ne soient pas si séparées de la partie présentation – je n'ai pas d'idée très précise en tête, mais par exemple la marge du texte pourrait contenir une bande de couleur identifiant les parties les plus activement éditées ou débattues.

Au risque de te faire avoir du mal avec toi-même, je suis d'accord avec toi! :)

C'est a mon avis un système beaucoup plus tenable que Wikipedia, qui essaie d'uniformiser l'opinion de la planète entière (au sein d'une communauté linguistique) pour convenir a tout le monde. Il y a un moment où ça ne fonctionne pas, il y a des conflits.

C'est vraiment le projet de Wikipédia? Écrire sans émettre d'opinion est presque complètement impossible, même si on peut faire des efforts pour essayer. Ce qui serait plus intéressant que des forks – le but ce n'est pas seulement que l'information existe mais aussi qu'elle soit accessible est trouvable – serait un sytème de commentaires, comme dans cette image:

On y voit un extrait manuscrit de la Bible au centre, avec des commentaires qui l'entourent. Par exemple les commentateurs de Wikipédia pourraient être des individus ou des groupes, l'idée étant que certaines présentations qui ne font pas consensus pourraient être insérées comme annotations. Le visiteur, lui, pourrait demander à voir les annotations faites par les commentateurs qui l'intéressent ou bien découvrir de nouveaux commentateurs.

C'est effectivement un usage qui change! En TeX il y a les commande \frenchspacing et \nofrenchspacing qui permettent de basculer!

— Les guillemets primaires sont les chevrons (« … »), parfois justement appelés guillemets français. Les guillemets anglais (double quotes) peuvent être utilisés comme guillemets de second niveau, pour introduire une citation à l’intérieur d’une citation. Le chevron ouvrant (resp. fermant) est suivi (resp. précédé) d’une espace fine insécable.

Je crois que l'expression consacrée est guillemets de second rang et on peut aussi utiliser les «simple quotes françaises» (si on ose dire) que sont ‹ ›.

— Un tiret cadratin qui ouvre une incise est précédé d’une espace inter-mots et suivi d’une espace insécable ; inversement, le tiret qui ferme l’incise, le cas échéant, est précédé d’une espace insécable et suivi d’une espace inter-mots.

Tandis qu'en anglais on n'utilise pas d'espace ni avant, ni après.

— Le deux-points (:) est précédé d’une espace insécable et suivi d’une espace inter-mots.

J'utilise une espace fine insécable, et du coup j'ai vérifié ce que fait la Pléiade et le Traité d'harmonie théorique et pratique de Théodore Dubois — ouvrage, qui comme son titre le suggère, a été préparé par un punk typographe — et ces deux références de qualitay utilisent l'espace fine avant les deux points.

— Le point-virgule, le point d’exclamation et le point d’interrogation sont précédés d’une espace fine insécable et suivis d’une espace inter-mots. Par extension, il devrait probablement en être de même pour les caractères non-officiels comme le point d’exclarrogation (‽) ou le point d’ironie (⸮).

Tandis qu'en anglais on ne met pas d'espace avant le signe (et pour le deux points c'est kif-kif).

— Les énumérations utilisent des tirets cadratins ou demi-cadratins, non des bullets.

Les pastilles (bullets) sont plutôt un usage américain tandis que les anglais ont un usage similaire aux français! ☺

Un point supplémentaire important est l'espace après le point final d'une phrase qui est différent en français et en anglais, en gros un espace simple pour dans le style français et une espace redoublée dans le style anglais.

C’est le fonctionnement par défaut de rsync qui utilise la date de modification et la taille pour savoir si un fichier a changé.

C'est différent parceque rsync a besoin d'avoir un fichier et sa copie pour faire cette comparaison alors que dump se contente de se souvenir qu'il a fait une sauvegarde du système de fichiers le 29 août 2015. On n'a même pas besoin de la sauvegarde précédente pour faire la prochaine (la sauvegarde précédente est dans le coffre fort;) )

Si la date ou la taille ne sont pas un critère fiable dans ton contexte, tu peux utiliser l’option --checksum de rsync et là oui, la comparaison avec un système encfs sur un sshfs va tout retélécharger, mais si la date ou la taille te suffisent, rsync fait ça très bien, de base, et le monatge encfs sur sshfs va seulement télécharger ce qui est nécessaire pour comparer les metadata.

Vu que rsync a un support ssh ce serait assez maladroit de ne pas en profiter et d'utiliser rsync à travers sshfs :)

Super ton document ! …

Il est quand-même un peu chargé, comme un solo de guitar hero très démonstratif.

1) Que conseilles-tu alors comme police libre pour des documents imprimés ?

J'aime beaucoup Palatino de Hermann Zapf, qui est dans un style très différend des caractères Garamond. Elle est d'apparence beaucoup moins raffinée que Garamond mais ses dessins sont très plaisants – les italiques sont particulièrement jolis – et supporte assez bien le rendu en faible résolution (écran d'ordinateur). LA version libre est URW Palladio et apparemment une relativement nouvelle s'appelle Pagella.

2) Niveau facilité de lecture sur un écran, j'avais cru comprendre que les standards changeaient,

La résolution d'un écran est bien plus basse que la résolution d'impression d'une imprimante bas de gamme. À titre d'exemple un Mac Book pro doté d'un écran dit Retina récent offre environ 220 PPP là où une imprimante jet d'encre à 50 € imprime sans problème à 360 PPP (600 PPP, 1200 PPP voire 2400 PPP pour du laser). Si on imprime à 2400 PPP c'est parceque l'œil humain est capable d'apprécier ce niveau de détail. Mon vieil écran VGA de 2002 a 72 DPI.

Imprimer en basse résolution (sur un écran p.ex.) est très difficile et très sensible aux erreurs d'arrondi. C'est pour ça notamment que longtemps les polices True-Type étaient affichées très mal par freetype, tout simplement parceque la spécification ne détermine pas complètement les méthodes de calcul et d'arrondi, ce qui explique une partie des différences avec l'implémentation TrueType de Micorsoft. Mais TrueType est désormais obsolète, donc…

Les empattements sont notamment des détails très fins qui vont mal supporter le rendu sur des supports à faible résolution. Beaucoup d'autre détails très subtils sont aussi malmenés par le rendu en basse résolution, comme l'ajustement des proximités ou des épaisseurs des traits pour fournir un joli gris. Sur ces types de support – mais aussi sur les supports destinés à être faxés par exemple! – il vaut mieux utiliser des caractères au dessin simple et un peu gras, comme par exemple certains sans-serif ou Times New Roman par exemple.

3) Pour le web, il y a beaucoup d'efforts en ce moment qui sont faits (le dernier sur lequel je suis tombé https://blot.im/typeset/). Sommes-nous sur les mêmes préférences que dans la question 2 pour de la lecture sur le web ?

En plus du support physique, la nature de la publication influence beaucoup. Par exemple j'ai un exemplaire du Canard près de moi, sur une page on peut trouver des articles écrits dans 5 fontes différentes (sur la page “la mare aux canards” je trouve deux fontes sans sérifs – gras et normal – et trois avec sérifs) ce qui aide probablement à distinguer entre les articles. Bref, c'est un métier!

Ensuite le public de lecture a son importance, car les formes des caractères véhiculent aussi un message et on ne va pas trouver les mêmes caractères sur une boutique en ligne d'un marchand de produits de luxe et d'un marchand de BMX.

Dans la famille Bush, il n'y a guère que le chien qui n'ait pas été candidat à la présidentielle. À part ça, le système est en pleine forme.

Tu peux aussi t'amuser avec ton petit parti, mais t'ira pas plus loin, les chiens de garde y veillent.

L'exemple du FN fondé en 1972 à partir d'essentiellement rien, comparé au parti-socialiste et les républicains, qui sont l'incarnation actuelles de regroupement politiques existant depuis plus d'un siècle montre que tu as tort.

C'est une voie sans issue. Sortie des principaux parties, tu ne seras JAMAIS élu(e).

Le but de l'élection présidentielle est d'éiir un président de la république qui assume ses fonctions pas de descerner un titre honorifique à une personne qui n'a en pratique aucun pouvoir politique et sera dans l'impossibilité de faire quoique ce soit. Si l'un d'entre Frédéric Nious, Nathalie Artaud ou Nicolas Dupont-Aignan se retrouvait élu président de la république, quel premier ministre nommerait il? Il faut qu'il soit accepté par le parlement! Donc il faudrait une alliance parlementaire du petit parti avec tout un tas de députés d'autres partis, dont fatalement la majorité viendront du PS ou de l'UMP. Si pour éviter ce scénario le nouveau président décidait de provoquer des élection législatives anticipées, il pourrait espérer rêver d'obtenir une majorité (quitte à faire de la fiction autant donner toutes les chances à notre nouveau président)… à condition d'aligner assez de candidats aux élections . Mais où les trouver? En faisant comme le FN qui a catapulté aux élections municipales des régiments entiers d'opportunistes qui ont suivi un crash-course de rhétorique et ont pour seul CV politique d'avoir été délégué de classe en quatrième et qui se rattachent à la commune qu'ils briguent parcequ'une arrière grand-tante a le même nom que la boulangerie en face de l'Église? Quelle perspective réjouissante!

Si un parti politique veut avoir une chance crédible de voir un de ses membres devenir président de la république, il faut en pratique que le parti en question ait un vrai poids politique (des élus municipaux, des députés, des sénateurs) et, comment dire, je ne peux pas m'empêcher de trouver ça bien.

Dump n'a pas besoin de rapatrier les données distantes pour faire de la vérification lors des sauvegardes incrémentelles parcequ'il utilise les dates de modification et travaille au niveau du système de fichiers (il suffit donc de se souvenir d'une date par système de fichiers).

Donc concrètement, tu dumpes, tu vérifies, tu chiffres et tu envoies.

De là à guérir du cancer en mangeant des pois chiches bios, faut pas déconner non plus :)

Des pois chiches peut-être pas, mais rien ne peut résister au kinoa rouge!