Mon prof de math justement, t'aurais mis 0, tu n'as pas indiqué la précision.
Il écrit des nombres décimaux, ce sont des valeurs tout a fait acceptables dont on n'a pas besoin d'indiquer la précision (sinon on indique un intervalle).
#install_printerQ.pp_print;;Q.(of_ints23*of_ints34);;(* 2/3 * 3/4 = 1/2 *)-:Q.t=1/2Q.(of_string"2"-of_string"18/10"-of_string"2/10");;(* 2 - 1.8 - 0.2 = 0 *)-:Q.t=0Q.(of_int2-of_float1.8-of_float0.2);;(* avec les float ça marche pas *)-:Q.t=-1/18014398509481984
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
D'autant que si on n'a pas déjà installé faketime, c'est plus long. Je ne sais pas comment fonctionne tous les systèmes, mais sur le mien ça ne fout pas le bordel. Si je n'enchaîne pas les deux commandes via le ;, mais l'une après l'autre, l'heure est déjà revenue à la normale.
$ date +%T -s "00:30:00"
00:30:00
$ man; date +%T
Quelle page de manuel voulez-vous ?
19:30:29
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Pour ma part, j'ai appris le système des bases en primaire. De mémoire, on avait un certain nombre de croix, de batons ou de points que l'on devait regrouper en ensemble de n éléments, puis on devait regrouper les groupes en surgroupes de n groupes, et ainsi de suite.
Itou. :-) De mémoire c'était surtout en CM1 et CM2 que l'on pratiquait ce genre d'analyse.
On avait également vu les règles de division par 3 ou 9 pour des nombres en base 10 avec compréhension de leur principe. Pour savoir si 54 est divisible par 3 (sans chercher dans ses tables ou effectuer la divison), il suffit de faire 5 + 4 = 9 et de constater que 9 est divisible par 3 donc 54 aussi. Le principe est simple quand on a compris le fonctionnement des bases : 54 c'est 5 paquets de dix et un paquet de 4. Or quand on divise un paquet de dix en trois personnes, chacun en a trois et il nous en reste un sur les bras. Donc avec cinq paquets, il nous en reste cinq sur les bras, plus les quatre unités cela fait neuf unités, que l'on peut alors répartir en trois par personnes.
Je me servais de ce genre de principe dans la cours quand on faisait du « plouf, plouf, amstramgram » pour choisir les membres de son équipe de foot : je savais par qui commencer pour avoir celui que je voulais, sans rien laisser au hasard. Les joies de l'arithmétique modulaire. :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Pour continuer sur le même exemple, combien de bacheliers sont bien à l'aise avec les changements de base (de numération) ? C'est pourtant ça le recul indispensable à enseigner les techniques opératoires élémentaires au CP.
Il y a du y avoir des changements, avec les époques, sur ce qui était enseigné tant aux élèves qu'aux enseignants. Si je prends mon expérience personnelle : dans les années 80, à la sortie de mon primaire on nous avait appris le changement de base (essentiellement la conversion base 10 vers base 5, mais des fois aussi base 2 ou 3). Lorsque j'étais étudiant, je donnais des cours particuliers pour financer mes études : certains de mes élèves de terminale (en terminale S) galéraient pour la conversion base 10 vers base 5. Et pour la formation de mes institutrices : la plupart avaient fait l'école normale sans être bachelières. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
D'après l'article d'Europe1, le communiqué de la Fédération des Aveugles de France contiendrait ce passage : « Pour nous personnes aveugles, cette soi-disant langue inclusive est proprement indéchiffrable par nos lecteurs d'écrans ». Je m'inscris totalement en faux contre cet argument en vertu du principe, déjà invoqué, suivant : « c'est pas compatible avec les lecteurs d'écran pour malvoyants » est un argument faux, émis par quelqu'un qui n'a jamais testé ces lecteurs. En effet, il va de soi que les aveugles n'ont jamais testé les lecteurs d'écran et sont les moins à même d'en parler. :-P
P.S : ceci étant dit, je n'ai pas réussi à trouver le communiqué en ligne sur leur site, bien que plusieurs journaux en parlent.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Un générateur d'onde sinusoïdale, dans le domaine audio, c'est proche d'un "Hello World!". ;-)
Après on peut jouer sur la fréquence ("Hello @hpiedcoq!") ou même la forme du signal ("@hpiedcoq, les sinusoïdes c'est la base du traitement du signal ;-)"). :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Si la phrase 'par la méthode de condorcet' fait partie de la discussion, on voit bien dans l'original anglais que c'est mentionné
Comme tu le soulignes, la référence à la méthode de scrutin à la Condorcet est mentionnée sur l'original chez Debian (fait qui est notoirement connu pour quiconque connaît un minimum le fonctionnement de l'organisation Debian).
Dans un commentaire de mon journal, je précise que la mention à cette méthode était un clin d'œil à certains journaux de l'époque (on était en pleine campagne présidentielle, et certains journaux parlaient de méthodes de votes alternatives). L'introduction même du journal est une allusion au contexte historique et aux débats de l'époque sur le site.
Dans un commentaire d'un de ces journaux, en date du 15 mai, je parle de Condorcet et Borda et de mon intérêt pour ces méthodes qui remonte au moins à l'élection de 2002 et le second tour Chirac - Le Pen.
Dans la dépêche, je développe cette partie sur les modes de scrutins avec lien vers un dossier sur le site Images des Maths du CNRS.
Je pense qu'il se peut fort bien que les deux soient de bonne foi
J'ai du mal à comprendre où l'on peut voir, de bonne foi, dans mon article (et sa version promue en dépêche) une contrefaçon du sien.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Pas du tout, à des souvenirs traumatisants du professeur qui ponctuait ses corrections par des références à l'évidence même sans réel explication.
Au temps pour moi, avec le sujet de la dépêche, j'ai du me sentir visé : dans l'autre journal j'avais fait un appel à l'évidence et tu m'avais répondu que même si cela paraissait évident, il fallait démontrer que la solution proposée apportait quelque chose.
Pour ce qui est de l'appel à l'évidence, dans l'enseignement, c'est toujours délicat : l'évidence est très subjective (ce qui est évident pour l'un, ne l'est pas forcément pour l'autre) et dans une correction, ce n'est pas le meilleur endroit pour y faire appel.
Ceci étant, même Coq a une notion d'évidence avec la tactique trivial :
Remarka:foralln,0+n=n+0.Proof.trivial.Qed.
mais en réalité, il trouve cela trivial car il applique directement un théorème qui est dans sa base de données (et qui énonce la même chose). En revanche, la preuve du théorème initial n'est pas triviale pour la machine, il faut la faire à la main par récurrence; là où avec un interlocuteur humain, un mathématicien serait tenté d'écrire : évident par récurrence sur n (en précisant toutefois le mode de démonstration à utiliser).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
C'est vrai que les justifications du type mais c'est évident ! ressemble fort à un prof de maths qui ne souhaite pas expliquer la solution en détails. :-)
Hé ! ce ne serait pas une allusion déguisée à certains de nos échanges récents sur un autre journal. :-P
Je ne suis pas prof de maths, et ce à quoi je faisais allusion c'est ce genre de chose :
extrait du livre ACSL by example (où ACSL signifie ANSI/ISO C Specification Langage). Il me semble évident que le système de type défini par ACSL est plus riche et permet de mieux exprimer la spécification de la fonction que ne le fait celui du langage C, qui dit juste que la fonction renvoie un booléen (ce que fait également la fonction qui renvoie constamment true). Qu'il existe un logiciel qui vérifie automatiquement que le code satisfait cette spécification, c'est un fait, il suffit de le tester.
Mais restons dans le sujet de la dépêche : la contrefaçon. Kant (oui, encore lui) a écrit un article sur le sujet en 1785 : De l'illégitimité de la contrefaçon des livres, article à la lecture fort intéressante et d'actualité, comme l'illustre la première note qui rappelle furieusement le problème des DRM :
Si un éditeur essayait de soumettre quiconque voudrait acheter son édition à la condition de se voir poursuivi pour soustraction d’un bien étranger à lui confié, dans le cas où, soit par son propre fait, soit par l’effet de sa négligence, l’exemplaire qu’il aurait acheté aurait été livré à l’impression, on n’y consentirait pas volontiers, car on ne voudrait pas s’exposer à toutes les importunités des perquisitions et des justifications. L’édition resterait donc sur les bras de l’éditeur.
Le texte est aussi une illustration de la rigueur, tant logique que juridique, avec laquelle Kant pouvait faire usage de la syllogistique.
Il reprendra, en 1797, le même thème dans sa Doctrine du droit dans un annexe aux droits des contrats sous le titre Qu'est-ce qu'un livre ?
La cause de ce qu'il y a d'apparamenent légitime dans une illégitimité qui saute pourtant aussi vivement aux yeux, du premier coup d'œil, que celle de la contrefaçon des livres, tient à ceci : le livre,d'une part, est un produit matériel de l'art (opus mechanicum) qui peut être imité (par celui qui se trouve en posséder légitimement un exemplaire, et par conséquent il y a là un droit réel; mais, d'un autre côté, le livre est aussi un pur et simple discours de l'éditeur au public, que le possesseur n'a pas le droit de reproduire publiquement (praestatio operae) sans avoir pour cela été mandaté par l'auteur — ce qui définit un droit personnel, et dans ces conditions l'erreur consiste en ce que l'on confond les deux droits.
Kant, Doctrine du Droit.
Sans entrée dans le détails, le droit des contrats relève du droit personnel (droit de contraindre une personne à une certaine prestation) et le genre d'annotations de code comme illustré ci-dessus est ce que l'on appelle la programmation par contrat. Elles expriment quelque chose du type : si les entrées vérifient certaines conditions alors la sortie en vérifiera d'autres. Il se trouve que Kant a donné pour fondements aux droits personnels la forme logique des jugements hypothétiques (si A alors B), tandis que les droits réels (droit de propriété sur une chose) ont pour fondements la forme logique des jugements catégoriques (A est B), ce qui correspond à la relation de sous-typage (comme je l'ai expliqué ailleurs).
Autrement dit, les débats sur la légitimité ou l'illégitimité de la contrefaçon tourne autour de la confusions entre la relation de sous-typage et le type d'une fonction.
En espérant que ce cas d'école illustrera ce que je voulais exprimer lorsque j'ai écrit un jour : ce que font les théories des types contemporaines, Kant le faisait déjà il y a plus de 200 ans. ;-)
Pour le détail, il faut se référer au contenu des théories concernées. :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Oui j'étais au courant, j'ai eu des échanges téléphoniques et par mails avec Benoît. En revanche je ne suis pas dans la procédure, il semble que je ne suis pas juridiquement impliqué dans l'affaire (bien que d'un point de vue moral, je le sois indubitablement). J'ai envoyé des éléments de défense pour nier la qualification de contrefaçon tant de l'article que de la dépêche.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Je ne sais pas quelle formation tu as eu, mais la question de la qualité dans le développement logiciel c'est loin d'être généralisé même aujourd'hui, que ce soit en entreprise ou dans les formations.
C'était une formation en logique mathématique et sur les fondements de l'informatique. Personnellement, à l'époque, la partie fondements de l'informatique ne m'intéressait pas spécialement. Je voulais surtout approfondir mes connaissances en logique et voir ce qu'avaient donné les attaques contre la philosophie kantienne des mathématiques (j'ai lu la Critique de la Raison Pure à la fin de ma spé, et je suis kantien depuis cette époque). Pour ceux intéressés par l'informatique, d'après la brochure sur les débouchés, il semblerait qu'ils finissent par faire une thèse et de la recherche (dans les organismes publiques ou en R&D chez des industriels genre EDF).
J'ai bien conscience qu'une telle formation est à part par rapport aux formations courantes des ingénieurs informaticiens.
Déjà, je dirais que pour être rigoureux intellectuellement, il faut démontrer que la solution proposée apporte quelque chose. Même si cela paraît évident. Car comme je l'ai dit, ce n'est pas parce que ton travail provient de la recherche universitaire que cela est forcément bénéfique. On ne va pas lister le nombre de prédictions théoriques de la recherche fondamentale (dont sur les noyaux de système d'exploitation) qui n'ont jamais su percer dans l'industrie faute d'adéquation en réalité.
Démontrer comment, par l'exemple ? Mais, de mon point de vue, un fait ne prouve pas grand chose : je m'intéresse surtout aux méthodes et à leur limite. Je suis un obsédé de la certitude : qu'est-ce que la certitude ? de quoi peut-on être certain ? quelles méthodes peuvent espérer atteindre à la certitude, lesquelles ne le peuvent pas ? font partie des questions qui m'obsèdent. Et de ce point de vue, l'induction et la méthode expérimentale reviennent à cela :
l'expérience ne donne jamais à ses jugements une universalité vraie et rigoureuse, mais seulement supposée ou comparative, si bien que cette universalité doit proprement signifier : Pour autant que nous l'ayons perçu jusqu'ici, il ne se trouve pas d'exception à telle ou telle règle.
Kant, introduction de la Critique de la Raison Pure.
ou pour citer Einstein résumant la philosophie sceptique de Hume : « l'empirique, dans la connaissance, n'est jamais certain (Hume) ». Il ne fut néanmoins pas convaincu par la réponse kantienne aux objections de Hume : « Kant propose alors une pensée. Sous la forme présentée elle est indéfendable mais elle marque un progrès nette pour résoudre le dilemme de Hume ». Pour ma part, je la trouve on ne plus défendable, et la méthode qu'il employa est analogue à celle utilisée par tous les systèmes de types des langages de programmations. Pour pousser le distinguo à l'extrême : je n'ai aucune certitude que le soleil se couchera se soir, mais je n'ai aucun doute quant à ce qu'exprime le théorème de Pythagore.
Pour revenir aux outils d'analyses et de sécurisation de code, il ne s'agit pas nécessairement de spécifier dans les moindres détails chaque bout de code et d'apporter la preuve du respect de la spécification, mais il est peut être envisageable d'ajouter certaines annotations en commentaires (à la manière de frama-c) pour avoir un système de type à l'expressivité plus riche que celui du C. Le système de type de C, de fait, exprime des spécifications sur le code mais, comme c'est peu ou prou la logique propositionnelle du premier ordre, on ne peut pas y exprimer grand chose : ce que fait le code et comment l'utiliser est beaucoup trop sous-spécifié avec un tel système de type.
Prenons un exemple. Je ne connaissais Coccinelle que de nom, je suis allé voir un peu leur site, et sur la page consacrée aux évolutions collatérales ils donnent deux exemple : ajout d'un argument à une fonction et changement dans le protocole d'initialisation des pilotes. Il semblerait que les pilotes aient mis un certain temps à s'adapter correctement à ce changement d'interface dans le cœur du noyau. Ces changements il faut bien les documenter quelque part ? Pourquoi pas dans une langue proche par sa syntaxe et son vocabulaire de l'anglais, mais à la grammaire plus régulière, et l'écrire en commentaire du code modifié ? On pourrait alors avoir une logiciel d'aide à l'audit qui détecterait automatiquement les mauvais usages des nouveaux codes.
Entre un audit totalement manuel et un audit partiellement automatisé, dans le monde de l'informatique ça doit pouvoir convaincre (pourquoi faire à la main ce qu'une machine peut faire pour moi ?). Je ne suis membre d'aucune des deux communautés (celle du noyau et celle de la recherche), mais je sais que la seconde est en état de fournir ce genre d'outil à la première. Néanmoins, pour cela, il faudrait une coopération et une synergie entre elles qui ne semblent pas exister aux dires de gasche. Je ne peux que trouver cela dommage.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Par contre, s'il y a un comportement indéfini du source, donc sémantique non définie, je pense pas que ça dise quoi que ce soit d'utile (on obtient juste un comportement « go wrong » accompagné d'une trace dès que la sémantique bloque, donc au mieux ça dirait peut-être que jusqu'au moment où ça bloque la sémantique est préservée).
C'est sur ce point que je ne sais pas ce qui est permis par le standard du C. Il y a des exemples de undefined behavior dans le manuel mais pas celle de l'exemple du journal : les exemples sont les overflow sur l'arithmétique signée (qui sont définies dans CompCert par les règles de l'arithmétique modulaire) et les accès hors bornes pour les tableaux qui renvoient une erreur.
D'après le deuxième principe que je cite du manuel « Second, the compiler is allowed to select one of the possible behaviors of the source program », le compilateur peut choisir n'importe quel comportement possible en accord avec la norme en cas de non déterminisme; c'est sur ce point que je n'ai pas bien compris si le choix de clang est acceptable (certains disent que oui, d'autres disent non) et pour moi cela reste encore bien obscur.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
La qualité du noyau (je dirais même la qualité logicielle au sens large), honnêtement, c'est assez récent comme problématique (moins de 5-10 ans), les choses se mettent en place et les progrès sont malgré tout importants.
Je suis étonné du caractère si récent de la prise en compte d'une telle problématique. J'ai terminé mes études il y a une quinzaine d'années et ce genre de questions étaient au cœur de la formation. Personnellement, l'utilité pour l'informatique était une chose qui, à l'époque, me semblait un cas d'application amusant mais sans plus; je regardais la chose d'un air amusé, les fondements des mathématiques m'important plus que ceux de l'informatique. Ce n'est que très récemment que je me suis repenché sur le lien avec le développement logiciel. À l'époque, les deux seuls langages que l'ont m'a enseigné était OCaml et Coq : avec le premier je m'étais amusé à faire un système de calcul formel sur l'arithmétique transfinie de Cantor, et avec le second j'avais formalisé quelques résultats élémentaires d'arithmétiques. Autant dire des questions de peut d'intérêt pour du développement logiciel.
Ceci étant dit, il est connu de longue date que la qualité logicielle relève de la preuve mathématique. Les approches dignes des sciences expérimentales à coup de tests unitaires ou de fuzzer, c'est gentil : ça peut détecter la présence de bugs, mais cela n'en prouvera jamais l'absence. À un moment, quand on affirme, il faut pouvoir prouver, quitte à le faire à la main :
Vous affirmez ? j'en suis fort aise.
Et bien ! prouvez maintenant.
pourrait être la devise des kantiens.
Quand je lis, par exemple, dans ce fil, que Nicolas Boulay demande qu'il faut démontrer la supériorité d'une solution avant de la mettre en œuvre et que gasche doit lui répondre :
Ce dont je parle ici (mais c'est loin d'être la seule sorte de recherche qui pourraitêtre utile au noyau) c'est d'éliminer, par des outils d'analyse, des classes entières de bugs possibles du code du noyau (use-after-free, accès à de la mémoire non initialisée, usage incorrect des verrous…). Tu écris comme si l'utilité de ce résultat final restait à démontrer, ce qui me semble complètement fou—évidemment c'est utile, et évidemment un noyau qui a su mettre ces outils en place va se retrouver loin devant un noyau qui ne l'a pas fait sur le long terme, en terme de robustesse et de qualité.
je tombe des nues. :-O Mais enfin, c'est une évidence pour qui est un minimum rigoureux intellectuellement ! On pourrait y rajouter en écho ce passage de l'évangile selon Saint Luc (chapitre 6, versets 47-49) :
47 Quiconque vient à moi, écoute mes paroles et les met en pratique, je vais vous montrer à qui il ressemble.
48 Il ressemble à celui qui construit une maison. Il a creusé très profond et il a posé les fondations sur le roc. Quand est venue l’inondation, le torrent s’est précipité sur cette maison, mais il n’a pas pu l’ébranler parce qu’elle était bien construite.
49 Mais celui qui a écouté et n’a pas mis en pratique ressemble à celui qui a construit sa maison à même le sol, sans fondations. Le torrent s’est précipité sur elle, et aussitôt elle s’est effondrée ; la destruction de cette maison a été complète. »
ou encore cet extrait de la préface des Prolégomènes à toute métaphysique future qui pourra se présenter comme science de Kant :
D'autre part il n'est pas tellement inouï qu'après avoir longtemps pratiqué une science, si on pense avec étonnement au progrès qui y a été accompli, on finisse par se poser la question de savoir si et comment de façon générale une telle science est possible. Car la raison humaine est assez désireuse de construire pour qu'il lui soit déjà maintes fois arrivé de bâtir la tour pour, puis de la démolir pour voir de quelle nature pouvait bien être son fondement. Il n'est jamais trop tard pour devenir sage et raisonnable; mais lorsque l'enquête est tardive, elle est plus difficile à mettre en train.
Lorsque gasche affirme que c'est un investissement sur le long terme :
Long terme: je pense que si les gens s'y mettaient sérieusement aujourd'hui il faudrait de l'ordre de 10-15 ans pour ça porte ses fruits.
cela va également de soi. Mais plus le projet tarde à s'y mettre, plus la base de code (déjà très volumineuse) augmentera et plus il sera difficile, voire surhumain, de mettre en pratique ce genre d'approche de contrôle qualité. Il vient donc naturellement à l'esprit cette question : la communauté en charge du développement du noyau est-elle sensible à ces questions ou s'en moque-t-elle fondamentalement ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Autant le code python me parle (je ne connais pas du tout ce langage), autant le DSL ne me parle pas.
Là, il y à un truc que je ne comprends pas du tout. Je n'avais pas prêté attention au message de ta part auquel gasche t'a répondu en présentant ce DSL, mais tu y reprochais à OCaml de ne pas générer des instructions SIMD en écrivant :
De plus, ocaml pourrait faire des map et fold sur des array de nombres, et proposer des versions vectorisés des opérations en question.
Il te répond avec un langage qui fait cela pour du code sur GPU, et tu réponds que ça ne te parle pas ? C'est quoi le problème ? Qu'ils utilisent la lettre pour définir des fonctions ? Qu'ils écrivent reduce et non fold ?
L'incompréhension venait du fait que le message de Renault pouvait être compris comme : « à partir de -O2 le compilateur se réservait le droit de modifier la sémantique d'un programme [qui possède une sémantique] ».
Tu n'es pas très joueur ! Moi, quand je m'ennuie, je joue à la roulette russe; ou en plus fun, je fais comme cap'tain sports extrêmes : je fais du saut à l'élastique mais sans élastique, avec un élastique on a aucune sensas' ! :-P
Pour prendre le manuel d'un compilateur qui ne s'amuse pas à changer la sémantique du code (« Traduttore, traditore » ou « Traducteur, traître » dit son manuel) :
There are three noteworthy points in the statement of semantic preservation above:
[…]
Second, the compiler is allowed to select one of the possible behaviors of the source program. The C language has some nondeterminism in expression evaluation order; different orders can result in several different observable behaviors. By choosing an evaluation order of its liking, the compiler implements one of these valid observable behaviors.
Third, the compiler is allowed to improve the behavior of the source program. Here, to improve means to convert a run-time error (such as crashing on an integer division by zero) into a more defined behavior. This can happen if the run-time error (e.g. division by zero) was optimized away (e.g. removed because the result of the division is unused). […]
et à la question « qu'est-ce qu'un comportement observable ? », il précise :
More precisely, we follow the ISO C standards in considering that we can observe:
Whether the program terminates or diverges (runs forever), and if it terminates, whether it terminates normally (by returning from the main function) or on an error (by running into an undefined behavior such as integer division by zero).
All calls to standard library functions that perform input/output, such as printf() or getchar().
All read and write accesses to global variables of volatile types. These variables can correspond to memory-mapped hardware devices, hence any read or write over such a variable is treated as an input/output operation.
Je ne connais pas bien la sémantique du C mais, pour l'exemple du journal, il me semble bien que l'optimisation de clang ne respecte pas ces principes.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Ceci est à mettre en parallèle avec les énoncés que l'on ferait sur l'encodage des entiers naturels dans ZF, où on écrirait pour énoncer une propriété des entiers. Ici le quantificateur universel sur x parcourt la collection de tous les ensembles (intreface{}) puis l'énoncé est une proposition hypothétique dont l'antécédent correspond à une vérification dynamique de type avant de continuer « l'exécution » vers le conséquent.
Et ça marche !! :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Au passage, je me demande s'il n'y a pas un lien avec une autre entrée de suivie que j'avais faite. Quand on met plusieurs formules en lignes et que l'on mélange avec du texte en chasse-fixe, elles ne sont pas toutes traitées.
Un test : le (d'où le \ de Haskell ou Elm) du lambda-calcul était à l'origine en majuscule .
Je veux bien essayer de voir d'où cela vient et tenter de corriger le problème, mais je ne sais pas par où commencer dans la base de code du site.
P.S : après prévisualisation, le test semble bien traiter le , mais ce n'est pas toujours le cas. Dans ce commentaire, j'ai un $x \in \omega$ non interprété en .
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
La non constructivité induit qu’il n’existe pas forcément de moyen de former un algorithme à partir du théorème ou de la formule, et c’est bien tout…
La correspondance s'étend aussi au raisonnement par l'absurde et donc à la logique classique, ce sont les exceptions dans les langages de programmation (les blocs try-with-finally). Voir ce texte de Jean-Louis Krivine (page 3).
Je crois que tu confonds « formule de la logique du premier ordre » et « logique du premier ordre ». Ou alors c’est moi qui confond…
Ce n'est qu'une question de vocabulaire : il y a d'un côté les jugements que l'on considère (calcul des prédicats ou calcul propositionnel, au premier ou second ordre) et de l'autre les règles de déductions (classique ou intuitionniste). Comme dans une logique on considère à la fois les règles de formations des jugements et les règles de déduction, pour éviter toute ambiguïté, il serait sans doute préférable de parler de logique classique du premier ordre et de logique intuitionniste du premier ordre.
Cela dit j’ai quand même l’impression d’être grugé. Dans un cas, le connecteur « -> » est vu par correspondance de curry-howard comme le type d’une fonction, alors que dans l’autre pour un langage dynamique tu as complètement oublié cette correspondance implication/fonction et c’est le quantificateur qui joue ce rôle.
Le quantificateur universel c'est le du lambda-calcul, le\ de Haskell, le fun de OCaml… c'est lui qui abstrait sur la totalité d'un domaine et, effectivement, dans le calcul des prédicats, on abstrait sur tout le domaine du modèle — sur tout l'univers des ensembles dans ZF. Les langages dynamiques sont des langages avec typage statique… qui n'ont qu'un seul type statique. Là où dans les théories des types, comme en Coq, on peut n'abstraire que sur les valeurs d'un type donné.
L'implication est bien toujours le signe d'une fonction mais, dans mon exemple, elle ne spécifie rien sur sa sortie pour une entrée qui n'est pas un ordinal. Si on reprend mon énoncé (légèrement modifié) :
il dit qu'à tout ensemble x, il peut en associer un autre y. Lorsque x est un ordinal, l'énoncé affirme que y est son prédécesseur qui est aussi un ordinal, mais dans le cas contraire (qui peut arriver, on a quantifié sur tous les ensembles), il ne dit rien sur y. La preuve d'un tel théorème expose, dans le cas où x est un ordinal, un moyen de produire un tel y et fournit la preuve que y est aussi un ordinal. En revanche, dans le cas où x n'est pas un ordinal, elle ne dit rien sur y (si ce n'est que c'est un ensemble, donc n'importe quelle valeur possible). Ce qui me fait penser à ce code Go :
funcpred(vinterface{})(uint,error){varresuintvarerrerrorswitchi:=v.(type){caseuint:ifi==0{res=uint(0)}else{res=uint(int(i)-1)}default:err=errors.New("not an uint")}returnres,err}
Il prend en entrée toute valeur possible (n'importe quel ensemble pour ZF), dans le cas où c'est un uint renvoie un y selon la même spécification que l'énoncé, ou bien renvoie une erreur si l'entrée n'est pas de type uint (cas de la preuve qui ne dit rien sur y, on renvoie une erreur). Ici le procédé est totalement constructif au sens des règles de déductions intuitionnistes. Le fait que la preuve du théorème prouve aussi que y est un ordinal, quand x l'est, se retrouve sur le type de sortie de la fonction en Go.
Après réflexion, on pourrait faire quelque chose de similaire en OCaml. Pour cela, il faut un type dans lequel on puisse plonger des valeurs de n'importe quel type : on parle de type universel. La signature d'un module fournissant un tel type est :
Je passe les détails d'implémentations d'un tel module (il faut utiliser un type somme extensible, comme l'est celui des exceptions dans le langage) et montre juste son usage en supposant que l'on a module U : Univ, c'est à dire un module fournissant un tel type :
(* ici on a des fonctions pour injecter dans et projeter * depuis le type `U.t` des valeurs de type `int` ou `nat` *)let(inj_int:int->U.t),proj_int=U.embed()let(inj_nat:nat->U.t),proj_nat=U.embed()(* on définit maintenant à partir de la fonction `pred` sur `nat` * une fonction `pred` générique sur le type universel `U.t` *)letpred_genv=matchproj_natvwith|None->None|Somen->Some(predn);;valpred_gen:U.t->natoption=<fun>(* si la valeur de type `U.t` contient un `int`, on renvoie `None` *)pred_gen(inj_int2);;-:natoption=None(* si elle contient un `nat`, on renvoie son prédecesseur *)pred_gen(inj_nat(S(SO)));;-:natoption=Some(SO)
Pour en revenir aux différentes logiques, le problème est bien dans le calcul des prédicats. Il est tel que, lorsqu'on l'interprète, toute les choses dont il parle sont considérées comme étant homogènes. Par exemple, si on veut formaliser la théorie des espaces vectoriels dans un tel symbolisme, il faut mettre les scalaires et les vecteurs dans un même sac fourre-tout et un modèle d'une telle théorie devra donner une signification à la somme d'un scalaire et d'un vecteur (ce qui, fondamentalement, n'a aucun sens dans un tel cadre). Raison pour laquelle je disais que les approches de la logique via la théorie des types captent bien mieux la notion de concept : le concept de scalaire ne sera nullement mélangé arbitrairement avec celui de vecteur, ce seront deux types distincts.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Je suis ingénieur, et je n'avais pas entendu parler de Lambda avant de faire un dea d'info.
Moi aussi, je n'avais jamais entendu parler de lambda-calcul avant mon DEA. Ce que je voulais dire, dans le fond, c'est que le niveau d'abstraction requis pour le comprendre relève du premier cycle en mathématique (une fois que l'on a expliqué ce que signifie le lambda, ce qui prend deux minutes). Tu trouves (si je me fie à ce que j'ai déjà lu) que elm est un bon langage pour faire du développement web : ce type de code doit être assez standard en elm. Elm a la même syntaxe que Haskell où le lambda est remplacé par l'anti-slash \, c'est tout. Après c'est du map-reduce, on ne peut plus classique en programmation fonctionnel, ce qui n'exige pas un niveau de compréhension d'un niveau doctoral.
En OCaml, on l'écrirait ainsi :
(* reduce c'est tout simplement fold_left *)letreduce=List.fold_left(* opérateur de composition infixe *)let(<.>)fg=funx->f(gx)letmap=List.mapletzip=List.combineletmul(a,b)=a*bletsum=reduce(+)0(* le lambda c'est le mot-clé fun *)letdot=funxsys->(sum<.>mapmul)(zipxsys)dot[1;2][3;4];;-:int=11
L'avantage pour des chercheurs de passer par du lambda-calcul, sans ajouter trop de sucre syntaxique, est d'avoir rapidement un prototype opérationnel comme preuve de concept.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Ca marche aussi... Mais j'ai triché
Posté par kantien . En réponse au journal [Humour] vers un monde différent. Évalué à 3.
mais les rationnels, eux, forment un corps :
:-)
et pour ceux qui aiment les grandes puissances :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Rien de surprenant
Posté par kantien . En réponse au journal [Humour] vers un monde différent. Évalué à 6.
Il écrit des nombres décimaux, ce sont des valeurs tout a fait acceptables dont on n'a pas besoin d'indiquer la précision (sinon on indique un intervalle).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Rien de surprenant
Posté par kantien . En réponse au journal [Humour] vers un monde différent. Évalué à 1.
Mauvais système de calcul formel ⇒ changer système de calcul formel :
Zarith :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: sans changer l'heure
Posté par kantien . En réponse au journal Que fait `man` passé minuit ?. Évalué à 3. Dernière modification le 30 novembre 2017 à 19:31.
D'autant que si on n'a pas déjà installé
faketime, c'est plus long. Je ne sais pas comment fonctionne tous les systèmes, mais sur le mien ça ne fout pas le bordel. Si je n'enchaîne pas les deux commandes via le;, mais l'une après l'autre, l'heure est déjà revenue à la normale.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: 00:01 ?
Posté par kantien . En réponse au journal Que fait `man` passé minuit ?. Évalué à 9.
Exact, il a du le modifier entre temps. Dans la version que j'ai c'est bien à minuit et demi. Voir le commit qui le retire.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Aigreur, quand tu nous tiens
Posté par kantien . En réponse au journal ils l'ont voulu, ils l'ont obtenu, et ils l'ont dans le baba.... Évalué à 6. Dernière modification le 24 novembre 2017 à 19:22.
Itou. :-) De mémoire c'était surtout en CM1 et CM2 que l'on pratiquait ce genre d'analyse.
On avait également vu les règles de division par 3 ou 9 pour des nombres en base 10 avec compréhension de leur principe. Pour savoir si 54 est divisible par 3 (sans chercher dans ses tables ou effectuer la divison), il suffit de faire
5 + 4 = 9et de constater que 9 est divisible par 3 donc 54 aussi. Le principe est simple quand on a compris le fonctionnement des bases : 54 c'est 5 paquets de dix et un paquet de 4. Or quand on divise un paquet de dix en trois personnes, chacun en a trois et il nous en reste un sur les bras. Donc avec cinq paquets, il nous en reste cinq sur les bras, plus les quatre unités cela fait neuf unités, que l'on peut alors répartir en trois par personnes.Je me servais de ce genre de principe dans la cours quand on faisait du « plouf, plouf, amstramgram » pour choisir les membres de son équipe de foot : je savais par qui commencer pour avoir celui que je voulais, sans rien laisser au hasard. Les joies de l'arithmétique modulaire. :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Aigreur, quand tu nous tiens
Posté par kantien . En réponse au journal ils l'ont voulu, ils l'ont obtenu, et ils l'ont dans le baba.... Évalué à 3. Dernière modification le 23 novembre 2017 à 11:44.
Il y a du y avoir des changements, avec les époques, sur ce qui était enseigné tant aux élèves qu'aux enseignants. Si je prends mon expérience personnelle : dans les années 80, à la sortie de mon primaire on nous avait appris le changement de base (essentiellement la conversion base 10 vers base 5, mais des fois aussi base 2 ou 3). Lorsque j'étais étudiant, je donnais des cours particuliers pour financer mes études : certains de mes élèves de terminale (en terminale S) galéraient pour la conversion base 10 vers base 5. Et pour la formation de mes institutrices : la plupart avaient fait l'école normale sans être bachelières. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Écriture
Posté par kantien . En réponse à la dépêche Quad9, résolveur DNS public, et sécurisé par TLS. Évalué à 5. Dernière modification le 21 novembre 2017 à 12:42.
D'après l'article d'Europe1, le communiqué de la Fédération des Aveugles de France contiendrait ce passage : « Pour nous personnes aveugles, cette soi-disant langue inclusive est proprement indéchiffrable par nos lecteurs d'écrans ». Je m'inscris totalement en faux contre cet argument en vertu du principe, déjà invoqué, suivant : « c'est pas compatible avec les lecteurs d'écran pour malvoyants » est un argument faux, émis par quelqu'un qui n'a jamais testé ces lecteurs. En effet, il va de soi que les aveugles n'ont jamais testé les lecteurs d'écran et sont les moins à même d'en parler. :-P
P.S : ceci étant dit, je n'ai pas réussi à trouver le communiqué en ligne sur leur site, bien que plusieurs journaux en parlent.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Hello world!
Posté par kantien . En réponse à la dépêche [Faust] Coder de l’audio en sifflotant. Évalué à 7.
Un générateur d'onde sinusoïdale, dans le domaine audio, c'est proche d'un "Hello World!". ;-)
Après on peut jouer sur la fréquence ("Hello @hpiedcoq!") ou même la forme du signal ("@hpiedcoq, les sinusoïdes c'est la base du traitement du signal ;-)"). :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: [HS] C'est lisible pour quelqu'un?
Posté par kantien . En réponse au journal Quad9, résolveur DNS public, et sécurisé par TLS. Évalué à 2.
Ça se discute, tout dépend à qui se réfère l'adjectif épithète. Ces trois phrases me semblent correctes, mais n'expriment pas la même chose :
dans la première, seule Marie Curie est qualifiée de brillante.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: 90 mots
Posté par kantien . En réponse à la dépêche Seconde mise en demeure pour l'association LinuxFr. Évalué à 10. Dernière modification le 14 novembre 2017 à 21:47.
Comme tu le soulignes, la référence à la méthode de scrutin à la Condorcet est mentionnée sur l'original chez Debian (fait qui est notoirement connu pour quiconque connaît un minimum le fonctionnement de l'organisation Debian).
Dans un commentaire de mon journal, je précise que la mention à cette méthode était un clin d'œil à certains journaux de l'époque (on était en pleine campagne présidentielle, et certains journaux parlaient de méthodes de votes alternatives). L'introduction même du journal est une allusion au contexte historique et aux débats de l'époque sur le site.
Dans un commentaire d'un de ces journaux, en date du 15 mai, je parle de Condorcet et Borda et de mon intérêt pour ces méthodes qui remonte au moins à l'élection de 2002 et le second tour Chirac - Le Pen.
Dans la dépêche, je développe cette partie sur les modes de scrutins avec lien vers un dossier sur le site Images des Maths du CNRS.
J'ai du mal à comprendre où l'on peut voir, de bonne foi, dans mon article (et sa version promue en dépêche) une contrefaçon du sien.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: l'assignation ne va jamais venir
Posté par kantien . En réponse à la dépêche Seconde mise en demeure pour l'association LinuxFr. Évalué à 4.
Au temps pour moi, avec le sujet de la dépêche, j'ai du me sentir visé : dans l'autre journal j'avais fait un appel à l'évidence et tu m'avais répondu que même si cela paraissait évident, il fallait démontrer que la solution proposée apportait quelque chose.
Pour ce qui est de l'appel à l'évidence, dans l'enseignement, c'est toujours délicat : l'évidence est très subjective (ce qui est évident pour l'un, ne l'est pas forcément pour l'autre) et dans une correction, ce n'est pas le meilleur endroit pour y faire appel.
Ceci étant, même Coq a une notion d'évidence avec la tactique
trivial:mais en réalité, il trouve cela trivial car il applique directement un théorème qui est dans sa base de données (et qui énonce la même chose). En revanche, la preuve du théorème initial n'est pas triviale pour la machine, il faut la faire à la main par récurrence; là où avec un interlocuteur humain, un mathématicien serait tenté d'écrire : évident par récurrence sur
n(en précisant toutefois le mode de démonstration à utiliser).Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: l'assignation ne va jamais venir
Posté par kantien . En réponse à la dépêche Seconde mise en demeure pour l'association LinuxFr. Évalué à 6.
Hé ! ce ne serait pas une allusion déguisée à certains de nos échanges récents sur un autre journal. :-P
Je ne suis pas prof de maths, et ce à quoi je faisais allusion c'est ce genre de chose :
extrait du livre ACSL by example (où ACSL signifie ANSI/ISO C Specification Langage). Il me semble évident que le système de type défini par ACSL est plus riche et permet de mieux exprimer la spécification de la fonction que ne le fait celui du langage C, qui dit juste que la fonction renvoie un booléen (ce que fait également la fonction qui renvoie constamment
true). Qu'il existe un logiciel qui vérifie automatiquement que le code satisfait cette spécification, c'est un fait, il suffit de le tester.Mais restons dans le sujet de la dépêche : la contrefaçon. Kant (oui, encore lui) a écrit un article sur le sujet en 1785 : De l'illégitimité de la contrefaçon des livres, article à la lecture fort intéressante et d'actualité, comme l'illustre la première note qui rappelle furieusement le problème des DRM :
Le texte est aussi une illustration de la rigueur, tant logique que juridique, avec laquelle Kant pouvait faire usage de la syllogistique.
Il reprendra, en 1797, le même thème dans sa Doctrine du droit dans un annexe aux droits des contrats sous le titre Qu'est-ce qu'un livre ?
Sans entrée dans le détails, le droit des contrats relève du droit personnel (droit de contraindre une personne à une certaine prestation) et le genre d'annotations de code comme illustré ci-dessus est ce que l'on appelle la programmation par contrat. Elles expriment quelque chose du type : si les entrées vérifient certaines conditions alors la sortie en vérifiera d'autres. Il se trouve que Kant a donné pour fondements aux droits personnels la forme logique des jugements hypothétiques (si A alors B), tandis que les droits réels (droit de propriété sur une chose) ont pour fondements la forme logique des jugements catégoriques (A est B), ce qui correspond à la relation de sous-typage (comme je l'ai expliqué ailleurs).
Autrement dit, les débats sur la légitimité ou l'illégitimité de la contrefaçon tourne autour de la confusions entre la relation de sous-typage et le type d'une fonction.
En espérant que ce cas d'école illustrera ce que je voulais exprimer lorsque j'ai écrit un jour : ce que font les théories des types contemporaines, Kant le faisait déjà il y a plus de 200 ans. ;-)
Pour le détail, il faut se référer au contenu des théories concernées. :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le plus malin est en général le premier qui cède
Posté par kantien . En réponse à la dépêche Seconde mise en demeure pour l'association LinuxFr. Évalué à 10.
Oui j'étais au courant, j'ai eu des échanges téléphoniques et par mails avec Benoît. En revanche je ne suis pas dans la procédure, il semble que je ne suis pas juridiquement impliqué dans l'affaire (bien que d'un point de vue moral, je le sois indubitablement). J'ai envoyé des éléments de défense pour nier la qualification de contrefaçon tant de l'article que de la dépêche.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le plus malin est en général le premier qui cède
Posté par kantien . En réponse à la dépêche Seconde mise en demeure pour l'association LinuxFr. Évalué à 10.
Ce qu'ils ont fait lors de sa promotion en dépêche.
Si le journal était purement factuel et reprenait la forme et le contenu de mes deux sources1 :
La dépêche (dont je suis également l'auteur) est autrement plus fouillée et détaillée, tandis que le journal s'apparente plus à une dépêche AFP.
Ce qui repose l'éternel débat sur le choix terminologique de linuxfr entre dépêche et journal. :-P
on notera que l'article de M. Gallaire n'en fait pas partie. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2. Dernière modification le 08 novembre 2017 à 12:31.
C'était une formation en logique mathématique et sur les fondements de l'informatique. Personnellement, à l'époque, la partie fondements de l'informatique ne m'intéressait pas spécialement. Je voulais surtout approfondir mes connaissances en logique et voir ce qu'avaient donné les attaques contre la philosophie kantienne des mathématiques (j'ai lu la Critique de la Raison Pure à la fin de ma spé, et je suis kantien depuis cette époque). Pour ceux intéressés par l'informatique, d'après la brochure sur les débouchés, il semblerait qu'ils finissent par faire une thèse et de la recherche (dans les organismes publiques ou en R&D chez des industriels genre EDF).
J'ai bien conscience qu'une telle formation est à part par rapport aux formations courantes des ingénieurs informaticiens.
Démontrer comment, par l'exemple ? Mais, de mon point de vue, un fait ne prouve pas grand chose : je m'intéresse surtout aux méthodes et à leur limite. Je suis un obsédé de la certitude : qu'est-ce que la certitude ? de quoi peut-on être certain ? quelles méthodes peuvent espérer atteindre à la certitude, lesquelles ne le peuvent pas ? font partie des questions qui m'obsèdent. Et de ce point de vue, l'induction et la méthode expérimentale reviennent à cela :
ou pour citer Einstein résumant la philosophie sceptique de Hume : « l'empirique, dans la connaissance, n'est jamais certain (Hume) ». Il ne fut néanmoins pas convaincu par la réponse kantienne aux objections de Hume : « Kant propose alors une pensée. Sous la forme présentée elle est indéfendable mais elle marque un progrès nette pour résoudre le dilemme de Hume ». Pour ma part, je la trouve on ne plus défendable, et la méthode qu'il employa est analogue à celle utilisée par tous les systèmes de types des langages de programmations. Pour pousser le distinguo à l'extrême : je n'ai aucune certitude que le soleil se couchera se soir, mais je n'ai aucun doute quant à ce qu'exprime le théorème de Pythagore.
Pour revenir aux outils d'analyses et de sécurisation de code, il ne s'agit pas nécessairement de spécifier dans les moindres détails chaque bout de code et d'apporter la preuve du respect de la spécification, mais il est peut être envisageable d'ajouter certaines annotations en commentaires (à la manière de frama-c) pour avoir un système de type à l'expressivité plus riche que celui du C. Le système de type de C, de fait, exprime des spécifications sur le code mais, comme c'est peu ou prou la logique propositionnelle du premier ordre, on ne peut pas y exprimer grand chose : ce que fait le code et comment l'utiliser est beaucoup trop sous-spécifié avec un tel système de type.
Prenons un exemple. Je ne connaissais Coccinelle que de nom, je suis allé voir un peu leur site, et sur la page consacrée aux évolutions collatérales ils donnent deux exemple : ajout d'un argument à une fonction et changement dans le protocole d'initialisation des pilotes. Il semblerait que les pilotes aient mis un certain temps à s'adapter correctement à ce changement d'interface dans le cœur du noyau. Ces changements il faut bien les documenter quelque part ? Pourquoi pas dans une langue proche par sa syntaxe et son vocabulaire de l'anglais, mais à la grammaire plus régulière, et l'écrire en commentaire du code modifié ? On pourrait alors avoir une logiciel d'aide à l'audit qui détecterait automatiquement les mauvais usages des nouveaux codes.
Entre un audit totalement manuel et un audit partiellement automatisé, dans le monde de l'informatique ça doit pouvoir convaincre (pourquoi faire à la main ce qu'une machine peut faire pour moi ?). Je ne suis membre d'aucune des deux communautés (celle du noyau et celle de la recherche), mais je sais que la seconde est en état de fournir ce genre d'outil à la première. Néanmoins, pour cela, il faudrait une coopération et une synergie entre elles qui ne semblent pas exister aux dires de gasche. Je ne peux que trouver cela dommage.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Comportement attendu
Posté par kantien . En réponse au journal Compilateur trop intelligent. Évalué à 2.
C'est sur ce point que je ne sais pas ce qui est permis par le standard du C. Il y a des exemples de undefined behavior dans le manuel mais pas celle de l'exemple du journal : les exemples sont les overflow sur l'arithmétique signée (qui sont définies dans CompCert par les règles de l'arithmétique modulaire) et les accès hors bornes pour les tableaux qui renvoient une erreur.
D'après le deuxième principe que je cite du manuel « Second, the compiler is allowed to select one of the possible behaviors of the source program », le compilateur peut choisir n'importe quel comportement possible en accord avec la norme en cas de non déterminisme; c'est sur ce point que je n'ai pas bien compris si le choix de clang est acceptable (certains disent que oui, d'autres disent non) et pour moi cela reste encore bien obscur.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Je suis étonné du caractère si récent de la prise en compte d'une telle problématique. J'ai terminé mes études il y a une quinzaine d'années et ce genre de questions étaient au cœur de la formation. Personnellement, l'utilité pour l'informatique était une chose qui, à l'époque, me semblait un cas d'application amusant mais sans plus; je regardais la chose d'un air amusé, les fondements des mathématiques m'important plus que ceux de l'informatique. Ce n'est que très récemment que je me suis repenché sur le lien avec le développement logiciel. À l'époque, les deux seuls langages que l'ont m'a enseigné était OCaml et Coq : avec le premier je m'étais amusé à faire un système de calcul formel sur l'arithmétique transfinie de Cantor, et avec le second j'avais formalisé quelques résultats élémentaires d'arithmétiques. Autant dire des questions de peut d'intérêt pour du développement logiciel.
Ceci étant dit, il est connu de longue date que la qualité logicielle relève de la preuve mathématique. Les approches dignes des sciences expérimentales à coup de tests unitaires ou de fuzzer, c'est gentil : ça peut détecter la présence de bugs, mais cela n'en prouvera jamais l'absence. À un moment, quand on affirme, il faut pouvoir prouver, quitte à le faire à la main :
pourrait être la devise des kantiens.
Quand je lis, par exemple, dans ce fil, que Nicolas Boulay demande qu'il faut démontrer la supériorité d'une solution avant de la mettre en œuvre et que gasche doit lui répondre :
je tombe des nues. :-O Mais enfin, c'est une évidence pour qui est un minimum rigoureux intellectuellement ! On pourrait y rajouter en écho ce passage de l'évangile selon Saint Luc (chapitre 6, versets 47-49) :
ou encore cet extrait de la préface des Prolégomènes à toute métaphysique future qui pourra se présenter comme science de Kant :
Lorsque gasche affirme que c'est un investissement sur le long terme :
cela va également de soi. Mais plus le projet tarde à s'y mettre, plus la base de code (déjà très volumineuse) augmentera et plus il sera difficile, voire surhumain, de mettre en pratique ce genre d'approche de contrôle qualité. Il vient donc naturellement à l'esprit cette question : la communauté en charge du développement du noyau est-elle sensible à ces questions ou s'en moque-t-elle fondamentalement ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 5.
Là, il y à un truc que je ne comprends pas du tout. Je n'avais pas prêté attention au message de ta part auquel gasche t'a répondu en présentant ce DSL, mais tu y reprochais à OCaml de ne pas générer des instructions SIMD en écrivant :
Il te répond avec un langage qui fait cela pour du code sur GPU, et tu réponds que ça ne te parle pas ? C'est quoi le problème ? Qu'ils utilisent la lettre
pour définir des fonctions ? Qu'ils écrivent
reduceet nonfold?Si j'écris cela :
alors tu comprends, mais tu voudrais que cela génère du code optimisé avec instructions SIMD ?
Mais quand on écrit :
alors tu ne comprends plus ?
On pourrait rendre le code python encore plus concis avec :
mais quand on sait ce qu'est un
fold(oureduce), unmapet une composition de fonctions, l'équivalence des deux écritures est évidente.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Comportement attendu
Posté par kantien . En réponse au journal Compilateur trop intelligent. Évalué à 4. Dernière modification le 04 novembre 2017 à 08:46.
Tu n'es pas très joueur ! Moi, quand je m'ennuie, je joue à la roulette russe; ou en plus fun, je fais comme cap'tain sports extrêmes : je fais du saut à l'élastique mais sans élastique, avec un élastique on a aucune sensas' ! :-P
Pour prendre le manuel d'un compilateur qui ne s'amuse pas à changer la sémantique du code (« Traduttore, traditore » ou « Traducteur, traître » dit son manuel) :
et à la question « qu'est-ce qu'un comportement observable ? », il précise :
Je ne connais pas bien la sémantique du C mais, pour l'exemple du journal, il me semble bien que l'optimisation de clang ne respecte pas ces principes.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Corrigé
Posté par kantien . En réponse à l’entrée du suivi Problème de parsing sur les formules latex. Évalué à 3 (+0/-0).
Merci ! :-)
Je teste :
Ceci est à mettre en parallèle avec les énoncés que l'on ferait sur l'encodage des entiers naturels dans ZF, où on écrirait
pour énoncer une propriété des entiers. Ici le quantificateur universel sur 
correspond à une vérification dynamique de type avant de continuer « l'exécution » vers le conséquent.
xparcourt la collection de tous les ensembles (intreface{}) puis l'énoncé est une proposition hypothétique dont l'antécédentEt ça marche !! :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Mieux ?
Posté par kantien . En réponse à l’entrée du suivi Impossible de répondre à un commentaire. Évalué à 2 (+0/-0).
Au passage, je me demande s'il n'y a pas un lien avec une autre entrée de suivie que j'avais faite. Quand on met plusieurs formules en lignes et que l'on mélange avec du texte en chasse-fixe, elles ne sont pas toutes traitées.
Un test : le
(d'où le 
.
\de Haskell ou Elm) du lambda-calcul était à l'origine en majusculeJe veux bien essayer de voir d'où cela vient et tenter de corriger le problème, mais je ne sais pas par où commencer dans la base de code du site.
P.S : après prévisualisation, le test semble bien traiter le
, mais ce n'est pas toujours le cas. Dans ce commentaire, j'ai un 
.
$x \in \omega$non interprété enSapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Mieux ?
Posté par kantien . En réponse à l’entrée du suivi Impossible de répondre à un commentaire. Évalué à 3 (+0/-0).
C'est bon, ça marche. Merci ! :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
La correspondance s'étend aussi au raisonnement par l'absurde et donc à la logique classique, ce sont les exceptions dans les langages de programmation (les blocs
try-with-finally). Voir ce texte de Jean-Louis Krivine (page 3).Ce n'est qu'une question de vocabulaire : il y a d'un côté les jugements que l'on considère (calcul des prédicats ou calcul propositionnel, au premier ou second ordre) et de l'autre les règles de déductions (classique ou intuitionniste). Comme dans une logique on considère à la fois les règles de formations des jugements et les règles de déduction, pour éviter toute ambiguïté, il serait sans doute préférable de parler de logique classique du premier ordre et de logique intuitionniste du premier ordre.
Le quantificateur universel c'est le
du lambda-calcul, le
\de Haskell, lefunde OCaml… c'est lui qui abstrait sur la totalité d'un domaine et, effectivement, dans le calcul des prédicats, on abstrait sur tout le domaine du modèle — sur tout l'univers des ensembles dans ZF. Les langages dynamiques sont des langages avec typage statique… qui n'ont qu'un seul type statique. Là où dans les théories des types, comme en Coq, on peut n'abstraire que sur les valeurs d'un type donné.L'implication est bien toujours le signe d'une fonction mais, dans mon exemple, elle ne spécifie rien sur sa sortie pour une entrée qui n'est pas un ordinal. Si on reprend mon énoncé (légèrement modifié) :
il dit qu'à tout ensemble
x, il peut en associer un autrey. Lorsquexest un ordinal, l'énoncé affirme queyest son prédécesseur qui est aussi un ordinal, mais dans le cas contraire (qui peut arriver, on a quantifié sur tous les ensembles), il ne dit rien sury. La preuve d'un tel théorème expose, dans le cas oùxest un ordinal, un moyen de produire un telyet fournit la preuve queyest aussi un ordinal. En revanche, dans le cas oùxn'est pas un ordinal, elle ne dit rien sury(si ce n'est que c'est un ensemble, donc n'importe quelle valeur possible). Ce qui me fait penser à ce code Go :Il prend en entrée toute valeur possible (n'importe quel ensemble pour ZF), dans le cas où c'est un
uintrenvoie unyselon la même spécification que l'énoncé, ou bien renvoie une erreur si l'entrée n'est pas de typeuint(cas de la preuve qui ne dit rien sury, on renvoie une erreur). Ici le procédé est totalement constructif au sens des règles de déductions intuitionnistes. Le fait que la preuve du théorème prouve aussi queyest un ordinal, quandxl'est, se retrouve sur le type de sortie de la fonction en Go.Après réflexion, on pourrait faire quelque chose de similaire en OCaml. Pour cela, il faut un type dans lequel on puisse plonger des valeurs de n'importe quel type : on parle de type universel. La signature d'un module fournissant un tel type est :
Je passe les détails d'implémentations d'un tel module (il faut utiliser un type somme extensible, comme l'est celui des exceptions dans le langage) et montre juste son usage en supposant que l'on a
module U : Univ, c'est à dire un module fournissant un tel type :Pour en revenir aux différentes logiques, le problème est bien dans le calcul des prédicats. Il est tel que, lorsqu'on l'interprète, toute les choses dont il parle sont considérées comme étant homogènes. Par exemple, si on veut formaliser la théorie des espaces vectoriels dans un tel symbolisme, il faut mettre les scalaires et les vecteurs dans un même sac fourre-tout et un modèle d'une telle théorie devra donner une signification à la somme d'un scalaire et d'un vecteur (ce qui, fondamentalement, n'a aucun sens dans un tel cadre). Raison pour laquelle je disais que les approches de la logique via la théorie des types captent bien mieux la notion de concept : le concept de scalaire ne sera nullement mélangé arbitrairement avec celui de vecteur, ce seront deux types distincts.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3. Dernière modification le 02 novembre 2017 à 15:07.
Moi aussi, je n'avais jamais entendu parler de lambda-calcul avant mon DEA. Ce que je voulais dire, dans le fond, c'est que le niveau d'abstraction requis pour le comprendre relève du premier cycle en mathématique (une fois que l'on a expliqué ce que signifie le lambda, ce qui prend deux minutes). Tu trouves (si je me fie à ce que j'ai déjà lu) que elm est un bon langage pour faire du développement web : ce type de code doit être assez standard en elm. Elm a la même syntaxe que Haskell où le lambda est remplacé par l'anti-slash
\, c'est tout. Après c'est du map-reduce, on ne peut plus classique en programmation fonctionnel, ce qui n'exige pas un niveau de compréhension d'un niveau doctoral.En OCaml, on l'écrirait ainsi :
L'avantage pour des chercheurs de passer par du lambda-calcul, sans ajouter trop de sucre syntaxique, est d'avoir rapidement un prototype opérationnel comme preuve de concept.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.