La gestation est arrivée à son terme ? J'espère pour ta femme que sa phase de travail n'a pas duré aussi longtemps. :-) Félicitations pour le petit (ou la petite).
Sinon pour faire une suggestion sur ton jeu. Dans ta dépêche tu demandes des retours sur les dessins vus de haut (personnages, autels…) et je trouve que cela rend assez bien, les arbres aussi. Par contre pour les terrains, la couleur uniforme (vert et marron) ça fait un peu « plat » et ça contraste avec les autres éléments. Ne pourrais tu pas voir avec David Tschumperlé pour faire des textures de terrains avec G'MIC ? Ça pourrait être sympa de voir deux projets, dont l'avancement est présenté régulièrement ici, coopérer.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Il y a d'autre part de la recherche en preuve pour les modèles distribués en utilisant des sémantiques de jeu, bien que cela soit au delà de mes compétences.
C'est à cela que je faisais référence, dans mon message à chimrod, quand je parlais du typage de protocoles réseau (et faire de la sémantique dénotationnelle dessus, en spécifiant la composition de deux protocoles à partir de leur sémantique respective ;-). Le lecteur intéressé pourra trouver un article, en français, sur la question sur hal où y sont exposés les principes de base de la démarche.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Mea culpa, je reconnais avoir été un peu sec dans mes réponses ce qui est un manque évident aux régles de bienséance, j'en suis désolé.
L'erreur est humaine, l'entêtement est diabolique (errare humanum est, perseverare diabolicum comme disent les latinistes), quelque soit le point sur lequel l'on se trouve pris en faute. Peu importe les torts réspéctifs de chacune des parties, l'important est la conciliation ou la réconciliation.
À l'origine de cette controverse, dispute ou discussion (choisis le mot qui te convient, peu m'importe) il y a effectivement, semble-t-il, une méprise. Je n'ai jamais, mais alors jamais, voulu dénigrer l'approche pragmatique par tests unitaires mais la critiquer, implicitement, cela est certain : mais la critique qui consiste à exposer les limites d'une méthode (ce qui sera à jamais en dehors de sa porté, et quand je dis jamais ce n'est pas parce que l'on ne sait pas faire aujourd'hui, mais parce l'on ne saura jamais faire certaine chose avec cette méthode, comme dans le théorème de Rice par exemple ;-) ne signifie pas le dénigrement (c'est nul, ça ne sert à rien et autres joyeusetés).
La pratique des tests unitaires est indispensable, comme approche, pour essayer de garantir le mieux que l'on peut que les programmes que l'on fait tourner sont corrects, dans la quasi-totalité des langage de programmation, et en OCaml particulièrement. Je n'aurai certainement pas contribuer à la rédaction de cette dépêche (la partie sur les améliorations du compilateur, avec chicco) si je considérai que la nécessité de reccourir à des tests unitaires en faisait un langage bon à mettre à la poubelle. ;-)
Le recours à des méthodes plus strictes et formelles pour garantir, avec certitude, qu'un code (ou un circuit) satisfait à ses spécifications n'est pas la panacée. Mais, contrairement à ce que tu crois, elles sont loin d'être un échec : et cela non uniquement dans les labarotoires de recherches, mais elles sont utilisées dans l'industriedepuis plus de vingt ans ! ;-) Et ce n'est pas le nombre d'acteurs industriels qui manquent : il me semblait avoir donné une liste importante dans ce message (et pas des moindres : IBM, Intel, Nasa, Agence Spatiale Européenne, Airbus…).
Pour te faire une meilleure idée de mes considérations sur les langages en informatique, je te propose la vidéo de cette conférence que j'avais abordée dans ma discussion avec chimrod.
Je me sens dans l'obligation de teaser un peu en commençant par sa conclusion : « j'espère avoir démonté l'idée qu'un langage est mieux que les autres, il y'en a qui sont moins bien que les autres ça c'est vrai, mais il n'y en pas qui sont mieux, il y a des choses différentes » (ce que j'exprimais, à ma façon, dans ce message en disant qu'il faut choisir l'outil adapté à ses besoins, ce qui nécessite de bien connaître ses besoins ainsi que les outils disponibles, leur qualités et leur faiblesses).
Il y a tout un passage tout à fait juste et assez comique sur les guerres de religion entre langage, dont voici la transcription de quelques diapos qu'il utilise :
L'imprératif
Détracteurs : l'impératif c'est un nid à bug, en particulier à cause des pointeurs et de la gestion mémoire par les utilisateurs
Partisans : Mais non, la programmation y est très naturelle, et il suffit d'y ajouter les assertions, les contrats, l'analyse statique, etc.
Le fonctionnel
Détracteurs : le fonctionnel, c'est pour les intellos, et c'est inefficace
Partisans : Mais non, ça demande juste un peu de culture scientifique, et l'inneficacité c'est du passé ! Le typage fort et la gestion automatique de la mémoire donne de la sécurité. Et on peut bien mieux raisonner sur les programmes, voire les prouver [là c'est moi qui graisse].
L'orienté objet
Détracteurs : L'objet c'est la fausse bonne idée : ça a l'air bien au début, mais il y a plein de problèmes (ex. héritage multiple) et c'est super-verbeux !
Partisans : Mais non ! l'héritage simple suffit le plus souvent, la programmation est naturelle et proche de l'architecture, elle passe bien à l'échelle, et le résultat est très efficace
La programmation logique qui a toujours était marginale
Détracteurs : La programmation logique et les contraintes, c'est bien joli, mais on ne sait jamais si ça va marcher et combien de temps ça va prendre !
Partisans (il précise « argument massue » dans la vidéo): Causez toujours, vous ne savez absolument pas faire ce que nous faisons !
Après avoir abordé les différents paradigmes, les principes du typage (dynamique ou statique) il conclue sur ces deux diapos :
Typage et vérification formelle
Typage dynamique : arrêter l'éxécution en cas de d'opération illégale (choux + carotte)—Scheme, Python, etc.
Typage Statique : dès la compilation, classifier les expressions selon les valeurs dénotées, et assurer la compatibilité des arguments des opérations
Vérification formelle : dès la compilation vérifier des propriétés quelconques (cf. séminaire de T. Jensen) [NdM : séminaire qui suit le sien, où T. Jensen présente essentiellement un système d'annotations ajouter dans les commentaires de code Java, ce que gasche a présenté comme solution par invariants et préconditions]
Que peut-on savoir sur le programme sans l'exécuter, et à quel prix ?
Intuition : le typage doit être très rapide
À l'oral, comme commentaire à la question centrale de la diapo, il ajoute « et ça quand on fait des avions c'est assez utile. S'il fallait débuguer les avions en les crachants [NdM : approche tests unitaires] ce serait moyen comme idée, mais on le fait un peu sur les bagnoles » (se souvenir de Airbus dans la liste des industriels ;-)
Et celle-là qui classifie les niveaux et différents systèmes de typage
Niveaux de typage
Interdire choux+carottes
Typer les fonctions et leurs applications : C, Java, etc.
Typer l'ordre supérieur (fonctions de fonctions)
Accpeter les types polymorphes (paramétriques)
Sous-typage (langage objets)
Inférence de types : trouver les bons types même lorsqu'ils ne sont pas écrits par le programmeur
Typage de modules et APIs : Programming in the large
Niveau maximal actuel : Coq, cf. cours du 18 mars 2015, types dépendants, typage garantissant la terminaison, mais l'inférence générale n'est plus décidable
Enfin, plus tôt dans sa conférence, il fait une allusion au langage B et B-event de Jean-Raymond Abrial qui les a utilisé pour certifier du code pour la RATP dans les années 90 (en l'occurrence, ceux qui empreintes la ligne 14, en tête là où il n'y a pas de chauffeurs et où on voit devant soit, il y a un ordinateur qui fait tourner du code B ;-).
Et M. Abrial avait présenté cette histoire en 2015 dans cette conférence dont voici le texte de 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.
J'en extrairai juste trois diapositives :
la première en plein dans le sujet de la discussion
la RATP décide de supprimer les tests unitaires et d'intégration
Octobre 98 : lancement de la ligne 14
Depuis lors pas de problèmes avec le logiciel développé avec [soit 17 ans plus tard, et il tourne, tourne, tourne…]
pour remplacer la démarche par
86.000 lignes en ADA ont été produites automatiquement
27.800 preuves ont été faites
92% ont été prouvés automatiquement par l'Atelier B
Coût des preuves interactives : 7 hommes-mois
Les preuves interactives sont moins chères que les tests
Conséquence de cette première historique (date d'ouverture en 1998, rappelons-le, donc je te laisse imaginer depuis quand les ingénieurs utilisaient ces outils ;-)
Métros utilsant B pour leurs développements : New York City, Amérique du Sud, Europe, Chine, etc.
Projets plus récents en France avec B :
Ligne 1 de la RATP à Paris (sans conducteur)
Navette de l'Aéroport Charles de Gaulle (sans conducteurs, 158.000 lignes en ADA, 43.600 preuves, 96.7% auto)
J'espère avoir montré que ces méthodes de certification formelles (en grande partie automatisée) sont loin d'être un « échec », et t'avoir donné envie (ainsi qu'à d'autres) d'aller jeter un œil sur ces deux conférences.
Le deuxième point est ton apprentissage individuel. Les personnes qui composent la communauté OCaml sont souvent des chercheurs qui ont un savoir assez impressionnant (et qui dépasse souvent le simple cadre de la communauté OCaml) se qui fait qu'il est toujours intéressant de discuter avec ces personnes qui vont te pointer vers des documents qui t'en apprendront plus sur les langages informatiques (domaine de prédilection d'OCaml), les algorithme et les paradigmes. L'avantage est qu'on garde toujours une réalité de ces connaissances qu'on peut appliquer (et qu'on applique) dans l'industrie. Ce qui fait que même si la courbe d'apprentissage est rude, elle n'en est pas moins impossible - par exemple, je viens tout droit d'un milieu très industriel (et j'ai ignoré presque tout les aspects théoriques de l'informatique) et pourtant j'arrive à m'en sortir en comprenant des concepts que je n'aurais jamais eu la chance de voir dans le milieu d'où je viens.
Il est vrai que les chercheurs (ou ceux qui ont des connaissances approchantes) aiment bien aider, même s'ils peuvent se montrer susceptibles ou soupe au lait quand ils ont l'impression que l'on cherche à leur expliquer des principes théoriques qu'ils connaissent bien et considèrent comme triviaux.
Sur ce, j'espère qu'après ces échanges nous nous quitterons bons amis. :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
On pourrait considérer la paire (programme, spécification) comme le programme (un programme annoté), mais la propriété que l'on veut vérifiée n'est pas exprimable en terme du langage reconnu par le programme annoté, ou plus généralement du comportement observable du programme annoté.
et donc les argumentations diagonales à la Cantor ne s'appliquent pas.
À la lecture de la réponse que tu as eu, j'abandonne la controverse. La prochaine fois j'éviterai les boutades sur Popper, tout est parti de là, d'autant que le recours à Popper semble se restreindre à la réfutation par le contre-exemple : si un test ne passe pas alors on a un contre-exemple donc le code n'est pas conforme à sa spécification1 (quand bien même elle n'est exprimée qu'informellemement); l'humanité n'a tout de même pas attendu Popper pour tenir ce genre de raisonnement.
Initialement je pointais du doigt l'inférence de type et son lien avec la déduction naturelle, ce que l'on peut faire automatiquement (sans annotation particulière du développeur, ni intervention de sa part dans le processus de dérviation) pour en pointer les limites (le théorème de Rice, si ça lui plaît) et là on a le droit à :
Je n'ai jamais dit que tous les problèmes non triviaux étaient indémontrables, j'ai seulement dit certain et cela depuis le début (bon effectivement ma phrase peut être perçu de manière ambigüe « des » signifie ici certain et non pas tous) et automatiquement (ie. par un compilateur générique)
Ce que personne n'a jamais nié, c'est même cette limite que je pointais du doigt. Il ne veut pas entendre que les conditions d'application du théorème sont dépassables (annotation, dérivation humaine avec assistance de la machine, système de types plus riche que le système F…), et donc que là où n'est pas la condition, là n'est pas le conditionné, i.e la conclusion du théorème.
Comme, de plus, j'interprète tous les problèmes autour du typage du lambda-calcul à travers le prisme de la correspondance de Curry-Howard, j'ai du mal à considérer la démonstration de théorèmes comme une science expérimentale et je suis du genre compilateur très pointilleux quand il s'agit d'en faire usage.
à ne pas confondre avec si tout les tests passent alors le code est conforme, sauf si les tests sont exhaustifs ce qui est impossible quand ils sont infinis; à moins de tester exhaustivement, non sur les instances des entrées, mais sur leur forme ce qui peut se faire en temps fini et ce que font les assistants de preuves. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Je répondais à quelqu'un qui disait que les tests unitaires étaient limités par rapport au raisonnement mathématique. Sauf qu'en vrai on a introduit les test unitaires parce que le raisonnement mathématique était limité (pas impossible, mais insuffisant).
Et je maintiens mes propos, sauf qu'on a introduit les tests unitaires parce que l'automatisation totale du raisonnement mathématique était limitée (on le savait déjà depuis Gödel, Rice n'est qu'une variante sur le même thème). Ce qui n'empêche pas de mettre en place des systèmes formels d'aide à la preuve où une partie est faite automatiquement par la machine, ou celle-ci aiguille le développeur qui effectue ce que la machine ne fait pas seule, et cela dans un langage où le système de type est bien plus expressif sur la sémantique du code (Coq en est l'exemple type).
Sans automatisation, en général les gens ne vont pas s'embêter à démontrer que le programme est correct car les preuves sont bien plus complexes que l'écriture de programme.
Cela dépend de l'aspect critique du programme, c'est comme pour tout il faut choisir l'outil adapté à ses besoins : on ne sort pas un char d'assaut pour écraser une mouche. Je n'ai jamais dit qu'utiliser des langages avec un expressivité sémantique limitée qui exigeait le recours aux tests unitaires étant sans intérêt, mais que des besoins pouvaient trouver cette approche insatisfaisante surtout que l'on sait faire plus sûr.
Ou encore tu pourrais expliquer l'inutilité (on va pas s'embêter à faire ça) de ce genre d'approche aux clients de AbsInt : Airbus, Esa, Nasa, Areva, Infineon, Continental, Thales, Bosch, BMW, Nokia, T-Systems, Intel, Compaq, Alliance Spacesystems, IBM, Sagem, Baxter, Healthcare Sanyo, Hewlett-Packard… perdre du temps est sans doute leur objectif premier.
Et on ne fait pas cela que sur des petits programmes, pour répondre au cas Arianne 5 et Rover, un compilateur C ce n'est pas ce que j'appelle un petit programme, mais Xavier Leroy doit lui aussi aimer s'embêter et perdre son temps.
Désolé mais je suis mon conciliant que gasche : ton utilisation du théorème de Rice est fumeuse.
(* le premier je le fais en deux temps *)letrecfx=fx;;valf:'a->'b=<fun>(*puis la je l'applique sur unit mais on peut prendre n'importe quoi *)f();;(* jolie boucle infinie, on fait Ctrl-C *)(* le second je le code en OCaml *)(* la fonction identité c'est la tautologie A ⇒ A *)letidx=x;;valid:'a->'a(* maintenant j'en fait une version restreinte avec un type fantôme *)typefaux;;letf(p:faux)=p;;valf:faux->faux
Le problème avec f serait de pouvoir l'appliquer (en faire usage) c'est à dire de pouvoir produire un terme de type faux alors que celui-ci est sans constructeur donc vide (ou inhabité).
Le passage de Rice à "les mathématiques ne sont pas possibles" est à mon avis un bel exemple d'extension abusive d'un résultat scientifique, comme on en lit souvent sur le théorème de Gödel ou sur la physique quantique. Je ne suis pas trop sûr de vers où part cette discussion.
Oula, il ne faut pas prendre la mouche. Mes reproches concernant l'epistémologie popperienne ne consistent pas simplement à dire qu'elle ne s'applique pas aux maths (je sais bien distinguer une science pure, d'une science expérimentale ;-). Mais là, le fil n'est pas un débat sur l'épistémologie : je pourrais, par exemple, lui reprocher plus précisément de ne pas porter assez attention aux principes non mathématiques, mais tout aussi purs, qui sont à la base des sciences expérimentales (principes métaphysiques) et qui échappent à sa démarche de falsification; ou bien de reconnaître, de son propre aveu, d'avoir emprunter sa conception de l'objet à Kant et celle de la vérité à Tarski alors qu'au fond Tarski ne dit rien de plus que Kant sur la notion de vérité, et que j'ai du mal à voir comment on peut comprendre sa conception de l'objet sans celle qu'il avait de la vérité (et donc, quel est l'intérêt de Tarski ?).
Je sais ce que sont les logiques classiques et intuitionnistes et leur rapport aux systèmes de typage : je l'ai déjà exposé ici; et oui, on peut transposer une preuve intuitionniste de l'irrationnalité de racine de 2 dans un système de typage : en la formalisant en Coq, par exemple.
Pour le troisième point, cela dépend : voir également mon commentaire cité au paragraphe précédent, ainsi que certains messages autour de la discussion qui l'a engendré (entre autre, pourquoi on ne peut pas se passer de tests unitaires en OCaml, mais qu'ils ne servent a priori à rien en Coq).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Cela est fort possible, je ne connais pas les problématiques d'optimisation liées à l'évaluation paresseuse (dans un terme (fun x -> une expression avec x) t, on substitue les occurrences de x par le terme t puis on beta-réduit et on mémoïse pour ne pas avoir à recalculer t si on en a nouveau besoin; là où OCaml commence par évaluer ou beta-réduire le terme t avant de substituer puis évaluer le tout). Mais effectivement comme un terme, dans les stratégies paresseuses, se trouve « pris » dans un thunk, cela doit rejoindre sur certains points la différence entre calcul flottant boxé et unboxé en OCaml.
Je voulais juste signaler que l'implémentation des optimisations décrites dans la dépêche doit prendre en compte la possibilité d'existence d'effets de bord permis par le langage (comme pour pouvoir propager un terme par exemple), ce qui n'est pas le cas en Haskell.
Il s'agit, il me semble, de deux problématiques d'optimisations orthogonales. D'ailleurs si on fait de l'évaluation paresseuse en OCaml (avec lazy et Lazy.force) cela doit être peu ou pas du tout optimisé, non ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Posté par kantien .
En réponse à la dépêche OCaml 4.03.
Évalué à 1.
Dernière modification le 03 mai 2016 à 19:20.
Tu avais noté mon commentaire dans un coin à l'époque (qui n'est pas si lointaine d'ailleurs…) ou tu l'as recherché aujourd'hui ? :)
Je l'avais noté dans un coin de ma tête, et je l'ai recherché aujourd'hui. Je m'en suis souvenu car à l'époque (pas si lointaine effectivement, sinon ce serait sans doute sorti de ma mémoire), j'avais fait des recherche pour savoir ce qu'est la SOA et comprendre ta problématique. J'en avais retenu l'idée qu'un WSDL est une façon de décrire la spécification d'un service, et qu'engendrer du code OCaml à partir de cela c'est similaire à de la transpilation.
Quand j'ai regardé encore plus récemment la vidéo de Gérard Berry (vraiment intéressante à regarder, je le conseille si on a le temps : 1h40 avec les questions du public), ça m'a rappelé mes réflexions sur le sujet et comme le sujet du TD est un cas pratique d'un principe plus général qui s'applique aussi à cette situation, je me suis dit : autant le partager.
Pour les problématiques de pédagogie et de didactique, je n'ai pas de réponse non plus, encore moins s'il s'agit d'informatique. La seule discipline que j'ai enseignée, il y a bien des années maintenant, dans le supérieur était les mathématiques; et ce que j'ai retenu de cette expérience est : je suis un bien piètre enseignant. :-/
Cela étant, en ce qui concerne la programmation et l'apprentissage d'un langage, l'approche par la pratique et on aborde les problèmes au fur et à mesure qu'on les rencontre de facto est sans doute moins rébarbatif et plus compréhensible.
Sinon, pourquoi faire de l'inférence de type sur papier ? ça doit être ennuyeux ? Je n'ai rien contre la théorie de la démonstration et la déduction naturelle, mais quand on apprend un langage de programmation ce ne doit pas être la première chose que l'on recherche, non ? Et il y a vraiment des gens qui présentent les tests unitaires en mettant un bouquin de Popper dans les mains de leurs étudiants ?
Sur Popper (j'ai du mal avec son principe de falsification) et les limites des tests unitaires ou des systèmes à inférence de type, j'aime bien le problème suivant : prouver avec certitude la non-existence d'une chose, comme la non-existence d'un couple d'entier dont le carré de l'un et le double du carré de l'autre (à savoir, prouver l'irrationalité de racine de 2). Problème résolu depuis l'époque des pythagoriciens… :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Posté par kantien .
En réponse à la dépêche OCaml 4.03.
Évalué à 1.
Dernière modification le 03 mai 2016 à 16:00.
Pourtant ce type de TD, et les notions abordées et mises en pratique à travers lui, pourrait t'être fort utile pour développer des bibliothèques qui ne font pas partie de l'écosystème OCaml et dont tu sembles avoir besoin. Je cite cet extrait de ton message de l'époque :
Mais il reste encore des points sur lesquels ces langages sont à la traîne (pas du point de vue technique, mais dans les librairie existantes). Surtout dans le domaine du web. Des choses auxquelles je pense :
La gestion des web service : à ma connaissance, OCaml n'a pas de bindings pour créer un client WS à partir d'un WSDL et garantir que les données transmises sont conformes.
La gestion du XML : j'aimerai beaucoup pouvoir garantir qu'une transformation XSL appliquée sur un schéma XSD d'entré me produit un XML conforme à un XSD de sortie. (quel que soit le xml bien sûr)
Tu ajoutais que c'est techniquement possible, ce qui est tout à fait vrai et met en pratique les mêmes idées que dans ton transpilateur : voir la conférence de Gerard Berry l'importance des langages en informatique. En particulier, pour le problème concerné, à partir de la 50ème minute1 : « il faut arrêter de penser qu'il y a une syntaxe concrète à un langage, la syntaxe abstraite doit commander : c'est elle la véritable syntaxe du langage. La syntaxe concrète ne doit être qu'une façon commode pour nous de représenter la syntaxe abstraite », suivi de « XML : une syntaxe concrète pour la syntaxe abstraite » et je rajouterai avec information de typage. ;-)
Cette vision du XML constitue aussi, dans un autre domaine, une des originalités de XMPP : les principes à la base des mécanismes de typage dans les langages comme OCaml s'étendent aux protocoles réseau (j'y avais fait allusion dans la discussion qui avait suivi ton message que j'ai cité), et on le retrouve dans la nature même des message échangés dans le fonctionnement d'XMPP. Je n'insinue pas que les concepteurs de XMPP avait cette idée en tête, je n'en sais absolument rien, ils ont peut être simplement fait comme M. Jourdain qui faisait bien de la prose sans le savoir…
cela étant, la totalité de la conférence mérite d'être regardée : elle est très instructive. :-) ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Posté par kantien .
En réponse à la dépêche OCaml 4.03.
Évalué à 3.
Dernière modification le 03 mai 2016 à 12:00.
Je confirme, sa présentation de la problématique était claire avec des exemples illustrant parfaitement les optimisations réalisables, une synthèse avec traduction étant amplement suffisante.
La présentation de Flambda sur le blog de jane street est aussi une lecture intéressante, en particulier sur les exemples choisis : différentes approches au niveau des paradigmes de programmation qui, néanmoins, génèrent le même code.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Je suis content de voir que le sujet de l'optimisation des performances est bien pris en compte, j'avais plusieurs fois entendu dire qu'il n'y avait que peu d'optimisation (qu'elles restaient haut niveau).
Les optimisations restent toujours haut niveau. Leur principe est connu depuis longtemps, elles n'étaient juste pas implémentées (ou pas de manière aussi poussée). In fine, ce sont somme toute des opérations élémentaires sur des termes du lambda-calcul : les réduction du l'ambda-calcul (sous-leur noms en apparences ésotériques, la beta-réduction, par exemple, est juste la transformation qui correspond à l'exécution du code, et c'est elle qui est utilisée en partie dans le processus d'inlining).
Contrairement à un langage fonctionnel pur comme Haskell, l'implémentation en OCaml demande plus de soin à cause de la manipulation de valeurs mutables. Mais ils restent encore des optimisations à effectuer, comme les opérations sur les flottants.
Certains auraient même souhaité l'intégration d'« assembleur » inline pour, par example, optimiser le calcul vectoriel en utilisant les jeux d'instuctions SSE.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
L'intêret de mon commentaire ? Où est le jugement ?
zurvan me dit que 150€ pour un téléphone ce n'est pas la mer à boire. Je lui objecte que ce tarif (pour quelqu'un qui a pas connu le monde antérieur, autrement qu'en tant qu'enfant) a de quoi suscité des interrogations. Et donc je réitère mon propos : où as-tu vu que 150€ pour un téléphone est une dépense standard ? Et tu appelles cela un jugement ?
Mon propos n'est pas de culpabiliser ceux qui peuvent se payer ce type d'outils (je le peux aussi, là n'est pas la question, et je ne me flagelle pas tous les soirs avant de me coucher), ni de dire que libre est synonyme de gratuit, mais de pointer du doigt que 150€ pour un téléphone, cela en fait rire plus d'un (rire surtout jaune).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Où est le mépris dans mon propos ? J'aimerais bien qu'on me le signale afin que je puisses adapter mon discours. Peut être n'avons nous pas la même notion du mépris.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Je ne suis pas Dieu, je n'ai pas les compétences (telle l'omniscience) pour faire ce genre de chose. ;-)
Sinon, je ne suis pas toujours d'accord en tout point avec l'auteur de l'article qui, bien qu'il s'en défend, fait de la réimportation du fondement de la doctrine libérale (elle trouve ses origines sur notre continent, mais elle a été en partie oubliée, puis elle fût en partie cultivée outre atlantique mais son retour est complètement défiguré).
L'auteur est aussi dans le comité de direction de L'institut Coppet qui est une réédition d'un institut ayant existé à la fin du 18ème et au début du 19ème, dont un des membres originels s'est trouvé pris dans une polémique avec Kant : pour moi, Kant en ressort vainqueur (polémique sur les notions de droits et de devoirs).
en moins de dix minutes.
On ne lit pas à la même vitesse.
C'est fort possible, mais je pense que c'est surtout parce que les questions abordées me sont familières donc ma « lecture » se limite surtout à du déchiffrement de signes alphabétiques.
Pour la promesse que je t'ai faite de réagir sur « vendre du libre », plus la discussion/dispute sur le sujet libre /open source, je crains de ne pouvoir la tenir : entendre par là que mes réponses ne seront pas faites aujourd'hui (je doute d'avoir le temps libre pour cela).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Mais on peut trouver des téléphones potables entre 150 et 300 €, par exemple à l'époque le nexus 4 (300 €) que j'ai gardé plus de 3 ans, le moto g (170 €) que j'ai conseillé à de nombreuses personnes etc.
Il n'y a rien qui te choque ?
Je n'ai jamais vraiment eu de téléphone avant d'Android apparaisse.
La réponse à ma question doit se trouver là. ;-)
P.S. : ce n'est pas une question d'android ou non, mais de smartphone = téléphone.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
C'est pas que je suis opposé à tes propos, sur le fil de la musique libre je te suivais un message sur deux; mais là, je ne comprends même pas ce que tu veux exprimer.
Pourtant je t'ai déjà vu intervenir sur des sujets qui abordés des erreurs de syntaxes et de grammaires, et sur le coup, ta syntaxe m'est incompréhensible : que veux-tu dire ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
N'importe quoi, les paquets synchronisés depuis Debian sont au minimum recompilés. Et Ubuntu a son propre noyau, ses propres versions d'un bon nombre de paquets, héberge toute son infrastructure, a une équipe dédiée au suivi de la sécurité…
Ils sont tellement recompilé que sur ma Debian, sans trop jouer l'enfer karmique est du passé (là, si on suit les principes, Debian torche Archelinux les doigts dans le nez), avec les back-ports cela passe pour les novices. Pour le reste, j'attends une meilleure solution.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Un petit supplément sur le libéralisme : celui qui croit que notre gouvernement actuel cède aux sirènes du libéralisme, que le politique de rigueur est libéral, celui-ci est, pour moi, comme un homme qui croit qu'un hacker est un cracker parce que c'est ce qu'on lui répète à longueur de journée.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
libéral regroupe beaucoup de tendances dont des gens qui ont le libéral sélectif (il y a des "libéraux" contre le mariage homo par exemple, ce qui n'est pas logique, ils se disent libéraux mais sont plutôt économiquement libéraux et socialement non libéraux). Perso je vois mal comment on peut être non libéral quand on est libriste, car c'est laisser les gens libres de faire des choses dans les deux cas (même en copyleft, si si).
Je dirai plutôt social-libéral si il faut catégoriser (la liberté des gens oui, mais avec un minimum de protection sociale type revenu universel et hôpitaux pour tous, car sans protection sociale pour donner une sécurité sur le vital point de liberté réelle)
C'est pour cela que j'avais mis un lien ;-) J'ai regardé les tiens, tu aurais pu regarder le mien; d'autant que les tiens sont des vidéos qui représentent 1h30 de temps, là où moi c'était un texte qui se lit en moins de dix minutes. Et tu aurais vu (ou plutôt lu) que les opposants aux mariages gay n'étaient pas ranger dans la catégorie « libéral » par les libéraux eux-mêmes, mais dans la catégorie « conservateur ».
Tu ne peux pas demander à autrui un acte (consulter les liens qu'il te propose et qui font partie de son discours, ce qui n'est rien d'autre qu'une liaison vers une bibliothèque externe) que tu ne fais pas toi même lorsqu'il te répond. ;-)
P.S. : je t'accorde, tout de même, que le terme « libéral » étant tellement galvaudé en France que je suis habitué à ce type de réponse. Le libéralisme n'est pas une doctrine économique, mais une doctrine juridique.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Tu ne serais pas un libéral pur jus par hasard (ce n'est pas un grief sous ma plume) ?
J'ai 2-3 questions à te poser sur la stratégie employée pour faire passer FFV1 auprès des archives autrichiennes, mais ça attendra demain (il y aura peut être du troll sur free / open source, demain c'est trolldi et tu as sacrément tendu la perche, mais je ferai en sorte de faire la part des choses1 ;-)
à moins que tu considères qu'il vaille mieux que je scinde mes propos en deux messages afin de ne pas brouiller inutilement la discussion (ce qui, à bien y réfléchir, est sans doute la meilleure solution). ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Mais en pratique, les entreprises préfèrent généralement demander une petit fonctionnalité qu'ils payeront plus ou moins cher, ou de la maintenance/support, ça passe mieux au niveau hiérarchique. Bref, l'administratif n'est pas un problème si en face le développeur le veut (asso, micro-entreprise… Ou vraie entreprise).
D'ailleurs, n'est-ce pas justement ce qu'il explique dans la première vidéo au sujet du codec FFV1 (vers la 35ème minute) quand l'Archive Nationale Autrichienne a voulu faire des archives sans perte ?
Bien que je n'ai pas tout compris au passage : il compare au choix de la bibliothèque du Congrès (qui a fait un choix propriétaire), puis il dit que les décisionnaires ont décidé d'allouer le budget à une solution propriétaire, pour finir par dire qu'il ont pris ffmpeg et payer pour des fonctionnalités, ce qui leur a coûté bien moins cher, et qu'avec l'argent qu'il restait ils ont pu payer un développeur pour améliorer leur infrastructure. Ils ont réussi à faire changer d'avis les décisionnaires ?
P.S : qui est donc ce lossless Lee ? :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Pour Java, oui, il y en a : je viens à l'instant de mettre à jour open-jdk sur ma Jessie.
De toute façon, un système sans faille de sécurité est un système dans lequel on n'a pas encore trouvé la faille. Rien que depuis le début de l'année chez Debian.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: La suite
Posté par kantien . En réponse à la dépêche Je crée mon jeu vidéo E16 : Nouveautés. Évalué à 4. Dernière modification le 07 mai 2016 à 23:24.
La gestation est arrivée à son terme ? J'espère pour ta femme que sa phase de travail n'a pas duré aussi longtemps. :-) Félicitations pour le petit (ou la petite).
Sinon pour faire une suggestion sur ton jeu. Dans ta dépêche tu demandes des retours sur les dessins vus de haut (personnages, autels…) et je trouve que cela rend assez bien, les arbres aussi. Par contre pour les terrains, la couleur uniforme (vert et marron) ça fait un peu « plat » et ça contraste avec les autres éléments. Ne pourrais tu pas voir avec David Tschumperlé pour faire des textures de terrains avec G'MIC ? Ça pourrait être sympa de voir deux projets, dont l'avancement est présenté régulièrement ici, coopérer.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 1.
C'est à cela que je faisais référence, dans mon message à chimrod, quand je parlais du typage de protocoles réseau (et faire de la sémantique dénotationnelle dessus, en spécifiant la composition de deux protocoles à partir de leur sémantique respective ;-). Le lecteur intéressé pourra trouver un article, en français, sur la question sur hal où y sont exposés les principes de base de la démarche.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 4.
Mea culpa, je reconnais avoir été un peu sec dans mes réponses ce qui est un manque évident aux régles de bienséance, j'en suis désolé.
L'erreur est humaine, l'entêtement est diabolique (errare humanum est, perseverare diabolicum comme disent les latinistes), quelque soit le point sur lequel l'on se trouve pris en faute. Peu importe les torts réspéctifs de chacune des parties, l'important est la conciliation ou la réconciliation.
À l'origine de cette controverse, dispute ou discussion (choisis le mot qui te convient, peu m'importe) il y a effectivement, semble-t-il, une méprise. Je n'ai jamais, mais alors jamais, voulu dénigrer l'approche pragmatique par tests unitaires mais la critiquer, implicitement, cela est certain : mais la critique qui consiste à exposer les limites d'une méthode (ce qui sera à jamais en dehors de sa porté, et quand je dis jamais ce n'est pas parce que l'on ne sait pas faire aujourd'hui, mais parce l'on ne saura jamais faire certaine chose avec cette méthode, comme dans le théorème de Rice par exemple ;-) ne signifie pas le dénigrement (c'est nul, ça ne sert à rien et autres joyeusetés).
La pratique des tests unitaires est indispensable, comme approche, pour essayer de garantir le mieux que l'on peut que les programmes que l'on fait tourner sont corrects, dans la quasi-totalité des langage de programmation, et en OCaml particulièrement. Je n'aurai certainement pas contribuer à la rédaction de cette dépêche (la partie sur les améliorations du compilateur, avec chicco) si je considérai que la nécessité de reccourir à des tests unitaires en faisait un langage bon à mettre à la poubelle. ;-)
Le recours à des méthodes plus strictes et formelles pour garantir, avec certitude, qu'un code (ou un circuit) satisfait à ses spécifications n'est pas la panacée. Mais, contrairement à ce que tu crois, elles sont loin d'être un échec : et cela non uniquement dans les labarotoires de recherches, mais elles sont utilisées dans l'industrie depuis plus de vingt ans ! ;-) Et ce n'est pas le nombre d'acteurs industriels qui manquent : il me semblait avoir donné une liste importante dans ce message (et pas des moindres : IBM, Intel, Nasa, Agence Spatiale Européenne, Airbus…).
Pour te faire une meilleure idée de mes considérations sur les langages en informatique, je te propose la vidéo de cette conférence que j'avais abordée dans ma discussion avec chimrod.
Je me sens dans l'obligation de teaser un peu en commençant par sa conclusion : « j'espère avoir démonté l'idée qu'un langage est mieux que les autres, il y'en a qui sont moins bien que les autres ça c'est vrai, mais il n'y en pas qui sont mieux, il y a des choses différentes » (ce que j'exprimais, à ma façon, dans ce message en disant qu'il faut choisir l'outil adapté à ses besoins, ce qui nécessite de bien connaître ses besoins ainsi que les outils disponibles, leur qualités et leur faiblesses).
Il y a tout un passage tout à fait juste et assez comique sur les guerres de religion entre langage, dont voici la transcription de quelques diapos qu'il utilise :
Après avoir abordé les différents paradigmes, les principes du typage (dynamique ou statique) il conclue sur ces deux diapos :
À l'oral, comme commentaire à la question centrale de la diapo, il ajoute « et ça quand on fait des avions c'est assez utile. S'il fallait débuguer les avions en les crachants [NdM : approche tests unitaires] ce serait moyen comme idée, mais on le fait un peu sur les bagnoles » (se souvenir de Airbus dans la liste des industriels ;-)
Et celle-là qui classifie les niveaux et différents systèmes de typage
Enfin, plus tôt dans sa conférence, il fait une allusion au langage B et B-event de Jean-Raymond Abrial qui les a utilisé pour certifier du code pour la RATP dans les années 90 (en l'occurrence, ceux qui empreintes la ligne 14, en tête là où il n'y a pas de chauffeurs et où on voit devant soit, il y a un ordinateur qui fait tourner du code B ;-).
Et M. Abrial avait présenté cette histoire en 2015 dans cette conférence dont voici le texte de présentation :
J'en extrairai juste trois diapositives :
la première en plein dans le sujet de la discussion
pour remplacer la démarche par
Conséquence de cette première historique (date d'ouverture en 1998, rappelons-le, donc je te laisse imaginer depuis quand les ingénieurs utilisaient ces outils ;-)
J'espère avoir montré que ces méthodes de certification formelles (en grande partie automatisée) sont loin d'être un « échec », et t'avoir donné envie (ainsi qu'à d'autres) d'aller jeter un œil sur ces deux conférences.
Pour conclure, je citerai un extrait du message de Dinosaure et y avoir en partie satisfait :
Il est vrai que les chercheurs (ou ceux qui ont des connaissances approchantes) aiment bien aider, même s'ils peuvent se montrer susceptibles ou soupe au lait quand ils ont l'impression que l'on cherche à leur expliquer des principes théoriques qu'ils connaissent bien et considèrent comme triviaux.
Sur ce, j'espère qu'après ces échanges nous nous quitterons bons amis. :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 0.
Pas mieux !
et donc les argumentations diagonales à la Cantor ne s'appliquent pas.
À la lecture de la réponse que tu as eu, j'abandonne la controverse. La prochaine fois j'éviterai les boutades sur Popper, tout est parti de là, d'autant que le recours à Popper semble se restreindre à la réfutation par le contre-exemple : si un test ne passe pas alors on a un contre-exemple donc le code n'est pas conforme à sa spécification1 (quand bien même elle n'est exprimée qu'informellemement); l'humanité n'a tout de même pas attendu Popper pour tenir ce genre de raisonnement.
Maintenant, on constate une technique du genre extension-restriction : le premier stratagème dans l'Art d'avoir toujours raison, avec un soupçon de « je mets de l'eau dans mon vin » sans en avoir l'air.
Initialement je pointais du doigt l'inférence de type et son lien avec la déduction naturelle, ce que l'on peut faire automatiquement (sans annotation particulière du développeur, ni intervention de sa part dans le processus de dérviation) pour en pointer les limites (le théorème de Rice, si ça lui plaît) et là on a le droit à :
Ce que personne n'a jamais nié, c'est même cette limite que je pointais du doigt. Il ne veut pas entendre que les conditions d'application du théorème sont dépassables (annotation, dérivation humaine avec assistance de la machine, système de types plus riche que le système F…), et donc que là où n'est pas la condition, là n'est pas le conditionné, i.e la conclusion du théorème.
Comme, de plus, j'interprète tous les problèmes autour du typage du lambda-calcul à travers le prisme de la correspondance de Curry-Howard, j'ai du mal à considérer la démonstration de théorèmes comme une science expérimentale et je suis du genre compilateur très pointilleux quand il s'agit d'en faire usage.
à ne pas confondre avec si tout les tests passent alors le code est conforme, sauf si les tests sont exhaustifs ce qui est impossible quand ils sont infinis; à moins de tester exhaustivement, non sur les instances des entrées, mais sur leur forme ce qui peut se faire en temps fini et ce que font les assistants de preuves. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 1.
Et je maintiens mes propos, sauf qu'on a introduit les tests unitaires parce que l'automatisation totale du raisonnement mathématique était limitée (on le savait déjà depuis Gödel, Rice n'est qu'une variante sur le même thème). Ce qui n'empêche pas de mettre en place des systèmes formels d'aide à la preuve où une partie est faite automatiquement par la machine, ou celle-ci aiguille le développeur qui effectue ce que la machine ne fait pas seule, et cela dans un langage où le système de type est bien plus expressif sur la sémantique du code (Coq en est l'exemple type).
Cela dépend de l'aspect critique du programme, c'est comme pour tout il faut choisir l'outil adapté à ses besoins : on ne sort pas un char d'assaut pour écraser une mouche. Je n'ai jamais dit qu'utiliser des langages avec un expressivité sémantique limitée qui exigeait le recours aux tests unitaires étant sans intérêt, mais que des besoins pouvaient trouver cette approche insatisfaisante surtout que l'on sait faire plus sûr.
Sinon, tu devrais en toucher deux mots à Gérard Berry dont les cours des deux dernière années au Collège de France ont été sur les thèmes : Prouver les programmes : pourquoi, quand, comment ? et Structures de données et algorithme pour la vérification formelle.
Ou encore tu pourrais expliquer l'inutilité (on va pas s'embêter à faire ça) de ce genre d'approche aux clients de AbsInt : Airbus, Esa, Nasa, Areva, Infineon, Continental, Thales, Bosch, BMW, Nokia, T-Systems, Intel, Compaq, Alliance Spacesystems, IBM, Sagem, Baxter, Healthcare Sanyo, Hewlett-Packard… perdre du temps est sans doute leur objectif premier.
Et on ne fait pas cela que sur des petits programmes, pour répondre au cas Arianne 5 et Rover, un compilateur C ce n'est pas ce que j'appelle un petit programme, mais Xavier Leroy doit lui aussi aimer s'embêter et perdre son temps.
Désolé mais je suis mon conciliant que gasche : ton utilisation du théorème de Rice est fumeuse.
Pour rebondir sur les deux exemples que t'a donné Burps.
Le problème avec
fserait de pouvoir l'appliquer (en faire usage) c'est à dire de pouvoir produire un terme de typefauxalors que celui-ci est sans constructeur donc vide (ou inhabité).Le second exemple porte un nom de sophisme bien connu : la pétition de principe, le premier étant le raisonnement circulaire qui n'en est qu'une variante. :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 2.
Tant que ça ne finit pas comme le théroème de Gödel ou une soirée avec M. Homais, même s'il a lui-même utilisé un argument diagonal à la Cantor. :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 1.
Oula, il ne faut pas prendre la mouche. Mes reproches concernant l'epistémologie popperienne ne consistent pas simplement à dire qu'elle ne s'applique pas aux maths (je sais bien distinguer une science pure, d'une science expérimentale ;-). Mais là, le fil n'est pas un débat sur l'épistémologie : je pourrais, par exemple, lui reprocher plus précisément de ne pas porter assez attention aux principes non mathématiques, mais tout aussi purs, qui sont à la base des sciences expérimentales (principes métaphysiques) et qui échappent à sa démarche de falsification; ou bien de reconnaître, de son propre aveu, d'avoir emprunter sa conception de l'objet à Kant et celle de la vérité à Tarski alors qu'au fond Tarski ne dit rien de plus que Kant sur la notion de vérité, et que j'ai du mal à voir comment on peut comprendre sa conception de l'objet sans celle qu'il avait de la vérité (et donc, quel est l'intérêt de Tarski ?).
Je sais ce que sont les logiques classiques et intuitionnistes et leur rapport aux systèmes de typage : je l'ai déjà exposé ici; et oui, on peut transposer une preuve intuitionniste de l'irrationnalité de racine de 2 dans un système de typage : en la formalisant en Coq, par exemple.
Pour le troisième point, cela dépend : voir également mon commentaire cité au paragraphe précédent, ainsi que certains messages autour de la discussion qui l'a engendré (entre autre, pourquoi on ne peut pas se passer de tests unitaires en OCaml, mais qu'ils ne servent a priori à rien en Coq).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Génial
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 3.
Cela est fort possible, je ne connais pas les problématiques d'optimisation liées à l'évaluation paresseuse (dans un terme
(fun x -> une expression avec x) t, on substitue les occurrences dexpar le termetpuis on beta-réduit et on mémoïse pour ne pas avoir à recalculertsi on en a nouveau besoin; là où OCaml commence par évaluer ou beta-réduire le termetavant de substituer puis évaluer le tout). Mais effectivement comme un terme, dans les stratégies paresseuses, se trouve « pris » dans un thunk, cela doit rejoindre sur certains points la différence entre calcul flottant boxé et unboxé en OCaml.Je voulais juste signaler que l'implémentation des optimisations décrites dans la dépêche doit prendre en compte la possibilité d'existence d'effets de bord permis par le langage (comme pour pouvoir propager un terme par exemple), ce qui n'est pas le cas en Haskell.
Il s'agit, il me semble, de deux problématiques d'optimisations orthogonales. D'ailleurs si on fait de l'évaluation paresseuse en OCaml (avec
lazyetLazy.force) cela doit être peu ou pas du tout optimisé, non ?Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 1. Dernière modification le 03 mai 2016 à 19:20.
Je l'avais noté dans un coin de ma tête, et je l'ai recherché aujourd'hui. Je m'en suis souvenu car à l'époque (pas si lointaine effectivement, sinon ce serait sans doute sorti de ma mémoire), j'avais fait des recherche pour savoir ce qu'est la SOA et comprendre ta problématique. J'en avais retenu l'idée qu'un WSDL est une façon de décrire la spécification d'un service, et qu'engendrer du code OCaml à partir de cela c'est similaire à de la transpilation.
Quand j'ai regardé encore plus récemment la vidéo de Gérard Berry (vraiment intéressante à regarder, je le conseille si on a le temps : 1h40 avec les questions du public), ça m'a rappelé mes réflexions sur le sujet et comme le sujet du TD est un cas pratique d'un principe plus général qui s'applique aussi à cette situation, je me suis dit : autant le partager.
Pour les problématiques de pédagogie et de didactique, je n'ai pas de réponse non plus, encore moins s'il s'agit d'informatique. La seule discipline que j'ai enseignée, il y a bien des années maintenant, dans le supérieur était les mathématiques; et ce que j'ai retenu de cette expérience est : je suis un bien piètre enseignant. :-/
Cela étant, en ce qui concerne la programmation et l'apprentissage d'un langage, l'approche par la pratique et on aborde les problèmes au fur et à mesure qu'on les rencontre de facto est sans doute moins rébarbatif et plus compréhensible.
Sinon, pourquoi faire de l'inférence de type sur papier ? ça doit être ennuyeux ? Je n'ai rien contre la théorie de la démonstration et la déduction naturelle, mais quand on apprend un langage de programmation ce ne doit pas être la première chose que l'on recherche, non ? Et il y a vraiment des gens qui présentent les tests unitaires en mettant un bouquin de Popper dans les mains de leurs étudiants ?
Sur Popper (j'ai du mal avec son principe de falsification) et les limites des tests unitaires ou des systèmes à inférence de type, j'aime bien le problème suivant : prouver avec certitude la non-existence d'une chose, comme la non-existence d'un couple d'entier dont le carré de l'un et le double du carré de l'autre (à savoir, prouver l'irrationalité de racine de 2). Problème résolu depuis l'époque des pythagoriciens… :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 1. Dernière modification le 03 mai 2016 à 16:00.
Pourtant ce type de TD, et les notions abordées et mises en pratique à travers lui, pourrait t'être fort utile pour développer des bibliothèques qui ne font pas partie de l'écosystème OCaml et dont tu sembles avoir besoin. Je cite cet extrait de ton message de l'époque :
Tu ajoutais que c'est techniquement possible, ce qui est tout à fait vrai et met en pratique les mêmes idées que dans ton transpilateur : voir la conférence de Gerard Berry l'importance des langages en informatique. En particulier, pour le problème concerné, à partir de la 50ème minute1 : « il faut arrêter de penser qu'il y a une syntaxe concrète à un langage, la syntaxe abstraite doit commander : c'est elle la véritable syntaxe du langage. La syntaxe concrète ne doit être qu'une façon commode pour nous de représenter la syntaxe abstraite », suivi de « XML : une syntaxe concrète pour la syntaxe abstraite » et je rajouterai avec information de typage. ;-)
Cette vision du XML constitue aussi, dans un autre domaine, une des originalités de XMPP : les principes à la base des mécanismes de typage dans les langages comme OCaml s'étendent aux protocoles réseau (j'y avais fait allusion dans la discussion qui avait suivi ton message que j'ai cité), et on le retrouve dans la nature même des message échangés dans le fonctionnement d'XMPP. Je n'insinue pas que les concepteurs de XMPP avait cette idée en tête, je n'en sais absolument rien, ils ont peut être simplement fait comme M. Jourdain qui faisait bien de la prose sans le savoir…
cela étant, la totalité de la conférence mérite d'être regardée : elle est très instructive. :-) ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Merci
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 3. Dernière modification le 03 mai 2016 à 12:00.
Je confirme, sa présentation de la problématique était claire avec des exemples illustrant parfaitement les optimisations réalisables, une synthèse avec traduction étant amplement suffisante.
La présentation de Flambda sur le blog de jane street est aussi une lecture intéressante, en particulier sur les exemples choisis : différentes approches au niveau des paradigmes de programmation qui, néanmoins, génèrent le même code.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Génial
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 3.
Les optimisations restent toujours haut niveau. Leur principe est connu depuis longtemps, elles n'étaient juste pas implémentées (ou pas de manière aussi poussée). In fine, ce sont somme toute des opérations élémentaires sur des termes du lambda-calcul : les réduction du l'ambda-calcul (sous-leur noms en apparences ésotériques, la beta-réduction, par exemple, est juste la transformation qui correspond à l'exécution du code, et c'est elle qui est utilisée en partie dans le processus d'inlining).
Contrairement à un langage fonctionnel pur comme Haskell, l'implémentation en OCaml demande plus de soin à cause de la manipulation de valeurs mutables. Mais ils restent encore des optimisations à effectuer, comme les opérations sur les flottants.
Certains auraient même souhaité l'intégration d'« assembleur » inline pour, par example, optimiser le calcul vectoriel en utilisant les jeux d'instuctions SSE.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Turing phone
Posté par kantien . En réponse au journal Enfin un téléphone haut de gamme sous Ubuntu Touch. Évalué à -2.
L'intêret de mon commentaire ? Où est le jugement ?
zurvan me dit que 150€ pour un téléphone ce n'est pas la mer à boire. Je lui objecte que ce tarif (pour quelqu'un qui a pas connu le monde antérieur, autrement qu'en tant qu'enfant) a de quoi suscité des interrogations. Et donc je réitère mon propos : où as-tu vu que 150€ pour un téléphone est une dépense standard ? Et tu appelles cela un jugement ?
Mon propos n'est pas de culpabiliser ceux qui peuvent se payer ce type d'outils (je le peux aussi, là n'est pas la question, et je ne me flagelle pas tous les soirs avant de me coucher), ni de dire que libre est synonyme de gratuit, mais de pointer du doigt que 150€ pour un téléphone, cela en fait rire plus d'un (rire surtout jaune).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Turing phone
Posté par kantien . En réponse au journal Enfin un téléphone haut de gamme sous Ubuntu Touch. Évalué à 0.
Où est le mépris dans mon propos ? J'aimerais bien qu'on me le signale afin que je puisses adapter mon discours. Peut être n'avons nous pas la même notion du mépris.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Turing phone
Posté par kantien . En réponse au journal Enfin un téléphone haut de gamme sous Ubuntu Touch. Évalué à -7.
On ne doit pas côtoyer les mêmes personnes…
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: HS micro-entreprise et les FUD dessus
Posté par kantien . En réponse au journal Libre ne veut pas dire gratuit : une présentation. Évalué à 1.
Je ne suis pas Dieu, je n'ai pas les compétences (telle l'omniscience) pour faire ce genre de chose. ;-)
Sinon, je ne suis pas toujours d'accord en tout point avec l'auteur de l'article qui, bien qu'il s'en défend, fait de la réimportation du fondement de la doctrine libérale (elle trouve ses origines sur notre continent, mais elle a été en partie oubliée, puis elle fût en partie cultivée outre atlantique mais son retour est complètement défiguré).
L'auteur est aussi dans le comité de direction de L'institut Coppet qui est une réédition d'un institut ayant existé à la fin du 18ème et au début du 19ème, dont un des membres originels s'est trouvé pris dans une polémique avec Kant : pour moi, Kant en ressort vainqueur (polémique sur les notions de droits et de devoirs).
C'est fort possible, mais je pense que c'est surtout parce que les questions abordées me sont familières donc ma « lecture » se limite surtout à du déchiffrement de signes alphabétiques.
Pour la promesse que je t'ai faite de réagir sur « vendre du libre », plus la discussion/dispute sur le sujet libre /open source, je crains de ne pouvoir la tenir : entendre par là que mes réponses ne seront pas faites aujourd'hui (je doute d'avoir le temps libre pour cela).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Turing phone
Posté par kantien . En réponse au journal Enfin un téléphone haut de gamme sous Ubuntu Touch. Évalué à -7. Dernière modification le 29 avril 2016 à 11:58.
Il n'y a rien qui te choque ?
La réponse à ma question doit se trouver là. ;-)
P.S. : ce n'est pas une question d'android ou non, mais de smartphone = téléphone.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Turing phone
Posté par kantien . En réponse au journal Enfin un téléphone haut de gamme sous Ubuntu Touch. Évalué à 1.
C'est pas que je suis opposé à tes propos, sur le fil de la musique libre je te suivais un message sur deux; mais là, je ne comprends même pas ce que tu veux exprimer.
Pourtant je t'ai déjà vu intervenir sur des sujets qui abordés des erreurs de syntaxes et de grammaires, et sur le coup, ta syntaxe m'est incompréhensible : que veux-tu dire ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Support 5 ans vs variantes
Posté par kantien . En réponse à la dépêche Sortie d’Ubuntu 16.04 LTS Xenial Xerus. Évalué à -4.
Ils sont tellement recompilé que sur ma Debian, sans trop jouer l'enfer karmique est du passé (là, si on suit les principes, Debian torche Archelinux les doigts dans le nez), avec les back-ports cela passe pour les novices. Pour le reste, j'attends une meilleure solution.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: HS micro-entreprise et les FUD dessus
Posté par kantien . En réponse au journal Libre ne veut pas dire gratuit : une présentation. Évalué à 4.
Un petit supplément sur le libéralisme : celui qui croit que notre gouvernement actuel cède aux sirènes du libéralisme, que le politique de rigueur est libéral, celui-ci est, pour moi, comme un homme qui croit qu'un hacker est un cracker parce que c'est ce qu'on lui répète à longueur de journée.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: HS micro-entreprise et les FUD dessus
Posté par kantien . En réponse au journal Libre ne veut pas dire gratuit : une présentation. Évalué à 2. Dernière modification le 29 avril 2016 à 00:34.
C'est pour cela que j'avais mis un lien ;-) J'ai regardé les tiens, tu aurais pu regarder le mien; d'autant que les tiens sont des vidéos qui représentent 1h30 de temps, là où moi c'était un texte qui se lit en moins de dix minutes. Et tu aurais vu (ou plutôt lu) que les opposants aux mariages gay n'étaient pas ranger dans la catégorie « libéral » par les libéraux eux-mêmes, mais dans la catégorie « conservateur ».
Tu ne peux pas demander à autrui un acte (consulter les liens qu'il te propose et qui font partie de son discours, ce qui n'est rien d'autre qu'une liaison vers une bibliothèque externe) que tu ne fais pas toi même lorsqu'il te répond. ;-)
P.S. : je t'accorde, tout de même, que le terme « libéral » étant tellement galvaudé en France que je suis habitué à ce type de réponse. Le libéralisme n'est pas une doctrine économique, mais une doctrine juridique.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: HS micro-entreprise et les FUD dessus
Posté par kantien . En réponse au journal Libre ne veut pas dire gratuit : une présentation. Évalué à 0.
Tu ne serais pas un libéral pur jus par hasard (ce n'est pas un grief sous ma plume) ?
J'ai 2-3 questions à te poser sur la stratégie employée pour faire passer FFV1 auprès des archives autrichiennes, mais ça attendra demain (il y aura peut être du troll sur free / open source, demain c'est trolldi et tu as sacrément tendu la perche, mais je ferai en sorte de faire la part des choses1 ;-)
à moins que tu considères qu'il vaille mieux que je scinde mes propos en deux messages afin de ne pas brouiller inutilement la discussion (ce qui, à bien y réfléchir, est sans doute la meilleure solution). ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: en entreprise
Posté par kantien . En réponse au journal Libre ne veut pas dire gratuit : une présentation. Évalué à 1. Dernière modification le 28 avril 2016 à 17:33.
D'ailleurs, n'est-ce pas justement ce qu'il explique dans la première vidéo au sujet du codec FFV1 (vers la 35ème minute) quand l'Archive Nationale Autrichienne a voulu faire des archives sans perte ?
Bien que je n'ai pas tout compris au passage : il compare au choix de la bibliothèque du Congrès (qui a fait un choix propriétaire), puis il dit que les décisionnaires ont décidé d'allouer le budget à une solution propriétaire, pour finir par dire qu'il ont pris ffmpeg et payer pour des fonctionnalités, ce qui leur a coûté bien moins cher, et qu'avec l'argent qu'il restait ils ont pu payer un développeur pour améliorer leur infrastructure. Ils ont réussi à faire changer d'avis les décisionnaires ?
P.S : qui est donc ce lossless Lee ? :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Turing phone
Posté par kantien . En réponse au journal Enfin un téléphone haut de gamme sous Ubuntu Touch. Évalué à 5. Dernière modification le 28 avril 2016 à 12:12.
Le problème c'est l'Empire ? Encore un sale coup du côté obscur de la Force !
Je m'en fous, comme droïde de protocoles, j'utilise C-3PO. En plus il peut me traduire toutes les langues connues de la galaxie. \o/
:-D
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Mir et Wayland périmés
Posté par kantien . En réponse à la dépêche Sortie d’Ubuntu 16.04 LTS Xenial Xerus. Évalué à 5.
Pour Java, oui, il y en a : je viens à l'instant de mettre à jour open-jdk sur ma Jessie.
De toute façon, un système sans faille de sécurité est un système dans lequel on n'a pas encore trouvé la faille. Rien que depuis le début de l'année chez Debian.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.