Ce que Kant a prouvé, par exemple, dans la Critique de la Raison Pure c'est que le concept de cause (qui sert à expliquer les changements d'états des choses réelles dans le monde physique) n'est pas un concept d'origine empirique, mais un concept que nous imposons nous même à la nature en vertu de la structure formelle de notre esprit
Mouais, je t’aurai suivi si tu avis dis que c’est une structure que nous suivons dans la manière dont nous représentons la nature (à la rigueur on peut modéliser les réseaux de neurones qui permettent d’anticiper les mouvements d’un projectile) mais quant-à plier la nature à la manière dont nous la représentons j’ai plus de doutes ;) Après effectivement on peut arguer que le cerveau fait des calculs de probabilité conditionnelles - http://www.college-de-france.fr/site/stanislas-dehaene/course-2012-02-21-09h30.htm très intéressant au passage - de là a dire que l’invention du concept de causalité est subordonnée à ça, ou si nous étions condamnés à l’inventer … Si notre propre observation de notre connaissance intuitive du mouvement (façon métacognition) nous prédestinait à inventer la causalité et à décrire le monde de cette façon, c’est possible par contre. Du coup c’est plutôt par l’émergence de système de survie efficace capable d’anticiper qu’il nous est apparu …
Enfin il faut faire attention à lier (si A alors B) avec un raisonnement causal, tu prends le risque de lier corrélation et causalité. « Si A alors B » en logique, c’est à chaque fois que A, on a B aussi. Pas « A cause B ». Tu parles sans doute des logiques constructives, spécifiquement, qui s’interprètent différemment ( https://en.wikipedia.org/wiki/Constructive_proof )
Ce que je voulais dire par « enrichis » c’est que Kant n’a jamais défini un de ces système formels. Par conséquences les jugements qui y sont afférents lui étaient inaccessibles. Tu peux arguer qu’il est possible de faire la même chose en langage naturel, mais il faut le contraindre de manière à ne garder que les jugements valides dans le système de règle défini. Or il n’a jamais décrit ces contraintes (enfin je te laisse l’infirmer ;).
Sinon d’accord, j’aurai probablement du dire, la cohérence dans l’axiomatique du modèle sous-jacent. Que l’on peut considérer comme vraie d«s lorsque qu’il en existe un modèle (au sens de la théorie des modèle) qui tient mathématiquement la route. Ce qui ne devrait pas être bien sorcier pour une théorie des types ou pour une logique du premier ordre.
Il y a quand même une légère différence dans les détails :) J’ai l’impression que tu décris une sorte de « principe de réflexion » de la pensée abstraite dans la logique formelle, comme dans l’univers constructible de Gôdel ( http://www.madore.org/~david/weblog/d.2013-03-19.2124.constructible.html ) ou les ensembles et leur structure décrit par un rang inférieur se reflètent dans les rangs supérieurs de différentes manières.
Les principes abstraits en langage naturel de Kant se reflètent dans les méthodes formelles modernes. Mais enrichis :)
Ne le prend pas mal, mais c’est de la naïveté. N’importe quel ingénieur sait qu’un composant a un domaine de validité et ne fonctionnera pas correctement en dehors. En informatique on a juste tendance à faire comme-ci on avait des vrais machine de Turing avec des bandes de mémoire illimitées. Ce n’est évidemment jamais le cas.
C’est juste que les données sont en général tellement petites qu’on peut faire « comme si » pour des kilos d’applications. Après dés que tu commences à jouer avec des algos exponentiels sur des problèmes NP-complets, tu comprends que c’est une fiction …
Ici, dans la recherche en langage de programmation, ils cherchent à encoder pas mal de choses dans les types. Ils ne seraient pas fâchés que par exemple on puisse coder ces règles métier dans les types, je pense. C’est un peu différent dans l’approche mais la méthode B permet d’en spécifier formellement dans l’invariant. Le truc pour ne pas avoir l’impression d’écrire plusieurs fois la même chose, c’est que la spec soit déclarative et de plus haut niveau que le code. Genre que la sortie d’une fonction qui a la propriété de trier c’est que chaque élément est inférieur au suivant. Ça te laisse complètement le choix de la manière de trier et ça va t’engueuler si t’as commenté l’appel au tri par erreur.
Si tu écris du code qui respectent pas ces règles encodées, l’objectif c’est que ça ne compile pas. Si tu écris deux règles qui sont incompatible l’une avec l’autre, logiquement, l’objectif est que ça te dise « t’es bien mignon mais c’est impossible de maintenir la propriété que la somme des surface est la somme de l’immeuble si tu modifie pas la taille de l’immeuble quand tu modifie la taille d’un appart » et que ça compile pas, itou. Ou alors que le département vente et le département fabrication utilisent pas la même notion de surface et que donc, les règles sont incohérentes et qu’il faut préciser le modèle.
Mais garde à l’esprit que c’est de la recherche en programmation qu’on parle ici. Il s’agit pas forcément d’avoir des choses utilisables dans la seconde.
Donc tu as un cas d’utilisation avec des arbres profonds pas profonds ? cqfd.
Tu es dnc ptete sur le cul mais t’es en plus à côté de la plaque ;) Moi ça me choque pas qu’un programme te dise honnêtement « je suis pas conçu pour ce genre de cas » et s’arrête. Ce qui me choquerait c’est que ça segfaulte salement. D’une manière générale, c’est pas une mauvaise pratique de fixer des limites.
Ben non justement, vérifier la cohérence interne veut dire que tu vérifie sans faire référence au monde extérieur que tes spécifications se tiennent elles mêmes et ne sont pas contradictoire en soi. Puis que ton programme est bien cohérent avec les spécifications.
Imagine que différents secteurs de l’entreprise aient différentes représentation d’un même produit. Elles n’ont pas la même vision, le service design, le service compta et le service marketing n’ont pas besoin des mèmes informations. Le SI peut par contre vérifier qu’il y a une certaine cohérence entre ces représentation.
En terme de cohérence, un ami m’a par exemple parlé d’un client promoteur en indiquant que le client voulait pas vraiment être sur que la surface disponible dans un immeuble était égale à la somme des surface des appartements. Dans le cas d’un client honnête, si il recherche à maintenir cette propriété, il est possible de vérifier que le programme garantit qu’un employé ne va pas aller tricher avec les données en bidouillant n’importe comment.
Le « modèle métier » c’est plutôt le modèle qui va te dire qu’un avion a en général deux ailes chez Airbus, ou que le débit et le crédit d’un compte bancaire doivent s’équilibrer chez un comptable.
Et c’est indépendant de la correction du compilateur, vu que c’est la cohérence «interne». La correction du compilateur garantit que ces propriétés seront préservées par la compilation.
La logique peut aussi vérifier la cohérence interne des connaissances des experts sur leur sujet. Mais effectivement elle va pas créer ex nihilo le modèle métier ou une théorie scientifique. Ça mettrai un paquet d’universitaires et d’informaticiens au chomage :) Mais du point de vue de la cohérence, ça peut lever des lièvres.
D’une manière générale, dire « aucune limite » c’est un raccourcis pour dire « toute la mémoire dispo ». En vrai, ça finira toujours par planter pour certains niveau d’imbrications - si c’est pas la pile qui explose, ce sera le tas. Si c’est pas le tas, ça sera le dd si t’as été pervers au point d’utiliser un fichier pour compter les accolades. Ça donne un fichier suffisamment grand pour toutes les applications réalistes, mais qui existe tout de même.
Et puis si t’en es à devoir traiter un arbre très très profond - alors que tout le point d’un arbre c’est en général de maintenir un certain niveau d’horizontalité et d’éviter de partir en profondeur (un index typiquement, que tu essayes de maintenir équilibré) t’as probablement d’autres préoccupations. Un arbres très profond, si on le suppose équilibré, ça veut dire que la taille des donnée est exponentiellement plus grande, donc absolument gigantesque. Peu de chances que ça termine dans un fichier json, en somme.
Un soucis de maturité des comportements sur LinuxFR ?
Et une culture chez certains contributeurs vis à vis de la sécurité je pense. Avec une idée « le seul moyen de corriger une faille c’est de l’exploiter » qui incite a des comportements complètement non naturels genre des comptes problématiques qui apparaissent opportunément pour troller. Ça incite à des postures excessivement défensives. Genre par crainte de de comportement détester jouer une caricature à la puissance 10 dudit comportement afin de pousser à l’interdire.
J’ajouterai perso que la théorie sur la sémantique d’un langage, ça devrait largement aider à construire un outillage puissant pour l’écosystème du langage.
L’exemple de l’inférence de type est un cas d’école, je pense : c’est une fonctionnalité très bien comprise théoriquement, qui permet d’aider le programmeur à faire moins d’erreur. La coloration syntaxique, c’est quand même utile d’avoir une grammaire formelle pour l’implémenter, et ces objets sont très bien connus théoriquement. Ça fait partie du baggage de base d’un informaticien. Peut être d’ailleurs qu’un des boulot du chercheur en langage c’est d’essayer de penser à des outils que la formalisation des langages peut aider à concevoir … après tout si c’est plus régulier et plus compréhensible pour les humains, c’est aussi très utile pour les machines pour raisonner sur le programme …
Ah oui pardon, j’ai dû être trompé par « Dans cette partie du texte, quand je parle de "voir un programme comme un objet mathématique", je parle plutôt du code source ». Toujours cette satanée confusion … c’est absolument pas naturel pour moi de considérer le code simplement comme un programme.
On est pas aidé par des expressions comme langage formel. En fait un langage de programmation (ou sa formalisation) est du côté des système formels, un langage formel en fait simplement partie. Le système formel est constitué du couple (langage formel, sémantique), et on est d’accord que la grammaire définit la partie « langage formel ».
Alors la façon dont je définis "un programme" c'est en donnant, par exemple, une syntaxe BNF qui, on est d'accord, correspond bien au choix d'un certain langage de programmation. Mais ce n'est pas à ce moment qu'on définit le langage, c'est seulement ensuite, une fois qu'on a défini ses programmes.
Ça se discute. Tu notes une relation de temporalité (voire de causalité) qui n’existe pas forcément dans le monde mathématiques. On ne définit pas les entiers en donnant tous les exemples d’entiers, et une fois qu’on l’a fait, on définit les entiers. On donne des axiomes qui permettent de décider si un objet du formalisme est ou pas un entier. Par l’axiome d’extensionnalité, à tout prédicat correspond une extension : « Étant donné un ensemble A et une propriété P exprimée dans le langage de la théorie des ensembles, il affirme l'existence de l'ensemble B des éléments de A vérifiant la propriété P »https://fr.wikipedia.org/wiki/Sch%C3%A9ma_d%27axiomes_de_compr%C3%A9hension . Mais à chaque propriété sur un ensemble correspond une seule extension … que tu définis « en même temps » que tu donnes la propriété. En complexité, on définit même un problème de décision comme l’appartenance ou pas d’une chaîne à un ensemble. Le prédicat associé à l’ensemble n’est même pas évoqué … En gros dans mon esprit la BNF (le prédicat) définit l’ensemble (le langage). Sauf si tu assimiles l’écriture de la BNF à la définition d’«un» programme, mais c’est pas du tout ma vision des choses. Enfin cette manière de décrire les choses correspond peut être à une vision constructiviste des choses ;).
Sinon je suis entièrement d’accord pour ce que tu dis sur la formalisation, avoir un accord parfait entre la théorie et l’expérience est un acte inaccessible. Cela dit, je pense avoir identifié un truc qui manque dans ton texte : il est considéré comme implicite que le programme est destiné à être exécuté. Du coup la métaphore du « parler » tombe un peu à plat. Quand je fais une requête google, je « parle » à la machine, pourtant je ne la programme pas. Un programme est destiné à être exécuté, et peut être exécuté pleins de fois. ça ne transparaît dans ton texte que quand tu parles de comportement du programme. Ce qui pourrait lever ton ambiguïté d’ailleurs.
(et je poste en l’état parce que j’y ai déjà passé trop de temps)
Je dirai que « les informaticiens ont inventé de nombreuses manières de décrire les programmes qui sont exécutés par un ordinateur » conviendrai dans un premier temps. Tu peux rajouter « souvent ils sont écris sous forme de texte, parfois d’autres formes, ou d’autres formes symboliques (« graphiques » par ex. https://scratch.mit.edu/) ». Dans tous les cas, le formalisme qui permet de les décrire constitue ce qu’on appelle un « langage de programmation ». »
L'idée c'est qu'on peut représenter un programme (dans un langage donné) comme un objet mathématique, et à partir de cela définir le langage.
Je comprend pas. Un programme écrit dans un langage donné est quelque part déjà un objet mathématique. « et à partir de cela définir le langage » euh, on commence pas par définir le langage avant d’écrire des programmes ??? Peut être qu’il faut que tu parles de sémantique (en général) d’un langage de programmation, sinon pareil je pense que ça peut ne pas être clair pour un débutant.
Je propose :
«Les informaticiens apprennent souvent par l’exemple et la pratique (et un prof et ses explications) ce qu’est supposé faire un programme et se forgent une intuition de la signification du code qu’ils écrivent, Ensuite, on essaye de le faire tourner pour voir si « ça marche » … et parfois, « ça marche ».
Les approches formelles s’appuient sur autre choses que l’essai et l’erreur et s’appuient sur la logique et les mathématiques pour décrire le comportement attendu d’un programme (indépendamment de ce qui se passe vraiment quand on le teste). La sémantique formelle (cette fois) d’un langage permet de faire le lien entre chaque programme écrit dans ce langage et ce comportement attendu. Votre boulot est en partie de l’écrire et de l’imaginer.»
Du coup vous vous nourrissez de la rigueur des maths pour détecter d’éventuels problèmes, et le point de vue différent offert peut donner de nouvelles idées et définir des choses précises là ou les langages de programmation « défini par l’implémentation ou la doc » sont moins précis et solides, peuvent avoir des trous et des points non documentés ou on est vraiment obligé de tester pour savoir ce que ça fait « en vrai ». Non ?
Intuitivement on pense à le définir comme un ensemble de programmes, mais en fait il faut aussi donner leur sémantique, c'est-à-dire donner le lien entre le programme (le texte) et le comportement quand on le lance (aussi représenté comme un objet mathématique.
« Intuitivement on pense à le définir comme un ensemble de programmes » Mmm certainement pas l’intuition d’un débutant … En fait ce que tu entend par « programme » n’est pas forcément clair. Et cette intuition de programme en tant que composition de programme interroge sur une notion de « programme primitif » qui est un peu HS et pas du tout intuitive pour quelqu’un qui ne connait pas la programmation. C’est un peu une impasse, je pense.
J’imagine que par « mathématiquement » tu veux dire « dans un formalisme logique ».
Attention, on peut aussi représenter mathématiquement un algorithme, mais l'objet mathématique qui correspond à un programme C par exemple n'est pas le même que celui qui correspond à l'algorithme implémenté
Il faut que tu utilises soit un langage algorithmique basique, qu’on peu facilement assimiler à un langage de programmation, soit des formules déclaratives (dans une logique) pour décrire des propriétés du résultats. La preuve visera à démontrer que les opérations décrites par l’algo réalisent bien les propriétés attendues. Ton utilisation de « mathématique » me gène en fait, en tant que personne qui connait un peu le domaine.
Autre remarque :
La sémantique d'un langage est alors donnée par une relation (mathématique) entre les programmes et leur comportement.
Je pense que c’est clair uniquement pour ceux qui savent ce qu’est une relation mathématique.
Ça n’absorbe pas grand chose si le papier finit cramé. Le CO2 est relargué relativement rapidement. Au mieux le bilan carbone de la filière est neutre si ces bois produisent suffisamment de matière pour l’industrie du papier, et en ignorant les énergies nécessaires au transport et à la fabrication du papier.
En plus pour des bouquins qui seront lus souvent une fois ou resteront invendus et termineront direct au pilon et au recyclage … voire prendront de la place et de la poussière dans une bibliothèque.
Cela dit j’aime bien le support papier, mais c’est pas ces forets d’exploitation qui vont le sauver. Le bilan d’une liseuse est probablement désastreux aussi, mais c’est sans doute mieux pour la forêt et la biodiversité en général. Petite pensée opur tous les auteurs qui ne sont pas Amélie Nothomb et qui peinent à se faire éditer aussi.
Je trouve ça dans l’ensemble très clair et très intéressant, même en étant pas la cible. Après je pense que la première phrase est un peu sèche pour un béotien (« représentation symbolique », ça peut faire peur, ce serait dommage). Et tu ne reparles pas de symbole dans la suite, donc l’utilité est sans doute discutable.
Quelques remarques :
Je pense aussi que tu peux intervertir « formalisation mathématique d'un langage de programmation » et « sémantique formelle ». Le second est plus technique, utiliser la première expression en définissant la seconde.
on lui donne une sémantique formelle (ou plusieurs) en définissant les programmes comme des objets mathématiques
Un peu ambigu je trouve, mais c’est pas très grave, et peut être un peu confusant : le programme peut être considéré comme la spécification d’un algorithme dans un langage, alors que la sémantique formelle peut être considérée comme la spec du langage lui même. Ou alors tu veux dire que si le langage n’a pas de sémantique formelle, on ne peut pas considérer le programme comme un objet mathématique ? Mais je pinaille peut être un peu beaucoup pour ce que tu cherches à faire.
L’idée c’est de débattre et de supprimer les silos, donc c’est fort possible. C’est presque le but. Mais l’idée ça a aussi l’air de pas refaire 43 milles fois le match, genre comme c’est possible en relançant un thread sur linuxfr ou tu vas dupliquer la même discussion.
Donc les farfelus, tout l’enjeu technique est de fournir des moyens de leur faire comprendre que le match à déjà eu lieux et que les arguments on déjà été donnés.
Je sais que ce n'est pas du tout ton objectif principal, mais si tu arrétais de personnaloser les débats àtpjt bout de champ ce serait quand même une bonne chose pour l'ambiance.
Il ne suffit pas de ne pas permettre des commentaires de résumé ?
Dans le papier il notent le fait qu’on note un début de «culture» du résumé avec les pratiques des participants qui s’alignent sur les pratiques des premier contributeurs du résumé, ça note que la communauté adopte une position pragmatique. Je pense que cette «culture» peut se bonifier avec l’expérience, et je pense aussi qu’elle se baserai sur l’intérêt communautaire bien compris (faire un résumé utile), et pas sur une volonté de discuter chaque virgule. En particulier, sur ce que tu dis, je pense qu’il s’agit de dépersonnaliser les arguments (ne pas évoquer « machin »), et mentionner le problème en question et ne pas le qualifier
Dans cette approche, j’ai l’impression que l’utilité est aussi de servir de « poteau indicateur » et de jouer le rôle de « sommaire » de la discussion.
[^] # Re: Le cerveau n'est pas logique
Posté par Thomas Douillard . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
Mouais, je t’aurai suivi si tu avis dis que c’est une structure que nous suivons dans la manière dont nous représentons la nature (à la rigueur on peut modéliser les réseaux de neurones qui permettent d’anticiper les mouvements d’un projectile) mais quant-à plier la nature à la manière dont nous la représentons j’ai plus de doutes ;) Après effectivement on peut arguer que le cerveau fait des calculs de probabilité conditionnelles - http://www.college-de-france.fr/site/stanislas-dehaene/course-2012-02-21-09h30.htm très intéressant au passage - de là a dire que l’invention du concept de causalité est subordonnée à ça, ou si nous étions condamnés à l’inventer … Si notre propre observation de notre connaissance intuitive du mouvement (façon métacognition) nous prédestinait à inventer la causalité et à décrire le monde de cette façon, c’est possible par contre. Du coup c’est plutôt par l’émergence de système de survie efficace capable d’anticiper qu’il nous est apparu …
Enfin il faut faire attention à lier (si A alors B) avec un raisonnement causal, tu prends le risque de lier corrélation et causalité. « Si A alors B » en logique, c’est à chaque fois que A, on a B aussi. Pas « A cause B ». Tu parles sans doute des logiques constructives, spécifiquement, qui s’interprètent différemment ( https://en.wikipedia.org/wiki/Constructive_proof )
Ce que je voulais dire par « enrichis » c’est que Kant n’a jamais défini un de ces système formels. Par conséquences les jugements qui y sont afférents lui étaient inaccessibles. Tu peux arguer qu’il est possible de faire la même chose en langage naturel, mais il faut le contraindre de manière à ne garder que les jugements valides dans le système de règle défini. Or il n’a jamais décrit ces contraintes (enfin je te laisse l’infirmer ;).
[^] # Re: Le cerveau n'est pas logique
Posté par Thomas Douillard . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
Sinon d’accord, j’aurai probablement du dire, la cohérence dans l’axiomatique du modèle sous-jacent. Que l’on peut considérer comme vraie d«s lorsque qu’il en existe un modèle (au sens de la théorie des modèle) qui tient mathématiquement la route. Ce qui ne devrait pas être bien sorcier pour une théorie des types ou pour une logique du premier ordre.
Sinon il semble que la définition de la cohérence comme absence de contradiction soit aussi communément admise. https://fr.wikipedia.org/wiki/Coh%C3%A9rence_(logique)
[^] # Re: Le cerveau n'est pas logique
Posté par Thomas Douillard . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
Il y a quand même une légère différence dans les détails :) J’ai l’impression que tu décris une sorte de « principe de réflexion » de la pensée abstraite dans la logique formelle, comme dans l’univers constructible de Gôdel ( http://www.madore.org/~david/weblog/d.2013-03-19.2124.constructible.html ) ou les ensembles et leur structure décrit par un rang inférieur se reflètent dans les rangs supérieurs de différentes manières.
Les principes abstraits en langage naturel de Kant se reflètent dans les méthodes formelles modernes. Mais enrichis :)
[^] # Re: Intérêt ?
Posté par Thomas Douillard . En réponse au journal Tous les parsers JSON sont mauvais. Évalué à 10.
Ne le prend pas mal, mais c’est de la naïveté. N’importe quel ingénieur sait qu’un composant a un domaine de validité et ne fonctionnera pas correctement en dehors. En informatique on a juste tendance à faire comme-ci on avait des vrais machine de Turing avec des bandes de mémoire illimitées. Ce n’est évidemment jamais le cas.
C’est juste que les données sont en général tellement petites qu’on peut faire « comme si » pour des kilos d’applications. Après dés que tu commences à jouer avec des algos exponentiels sur des problèmes NP-complets, tu comprends que c’est une fiction …
[^] # Re: Le cerveau n'est pas logique
Posté par Thomas Douillard . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Ici, dans la recherche en langage de programmation, ils cherchent à encoder pas mal de choses dans les types. Ils ne seraient pas fâchés que par exemple on puisse coder ces règles métier dans les types, je pense. C’est un peu différent dans l’approche mais la méthode B permet d’en spécifier formellement dans l’invariant. Le truc pour ne pas avoir l’impression d’écrire plusieurs fois la même chose, c’est que la spec soit déclarative et de plus haut niveau que le code. Genre que la sortie d’une fonction qui a la propriété de trier c’est que chaque élément est inférieur au suivant. Ça te laisse complètement le choix de la manière de trier et ça va t’engueuler si t’as commenté l’appel au tri par erreur.
Si tu écris du code qui respectent pas ces règles encodées, l’objectif c’est que ça ne compile pas. Si tu écris deux règles qui sont incompatible l’une avec l’autre, logiquement, l’objectif est que ça te dise « t’es bien mignon mais c’est impossible de maintenir la propriété que la somme des surface est la somme de l’immeuble si tu modifie pas la taille de l’immeuble quand tu modifie la taille d’un appart » et que ça compile pas, itou. Ou alors que le département vente et le département fabrication utilisent pas la même notion de surface et que donc, les règles sont incohérentes et qu’il faut préciser le modèle.
Mais garde à l’esprit que c’est de la recherche en programmation qu’on parle ici. Il s’agit pas forcément d’avoir des choses utilisables dans la seconde.
[^] # Re: Intérêt ?
Posté par Thomas Douillard . En réponse au journal Tous les parsers JSON sont mauvais. Évalué à 7.
Donc tu as un cas d’utilisation avec des arbres profonds pas profonds ? cqfd.
Tu es dnc ptete sur le cul mais t’es en plus à côté de la plaque ;) Moi ça me choque pas qu’un programme te dise honnêtement « je suis pas conçu pour ce genre de cas » et s’arrête. Ce qui me choquerait c’est que ça segfaulte salement. D’une manière générale, c’est pas une mauvaise pratique de fixer des limites.
[^] # Re: Le cerveau n'est pas logique
Posté par Thomas Douillard . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Ben non justement, vérifier la cohérence interne veut dire que tu vérifie sans faire référence au monde extérieur que tes spécifications se tiennent elles mêmes et ne sont pas contradictoire en soi. Puis que ton programme est bien cohérent avec les spécifications.
Imagine que différents secteurs de l’entreprise aient différentes représentation d’un même produit. Elles n’ont pas la même vision, le service design, le service compta et le service marketing n’ont pas besoin des mèmes informations. Le SI peut par contre vérifier qu’il y a une certaine cohérence entre ces représentation.
En terme de cohérence, un ami m’a par exemple parlé d’un client promoteur en indiquant que le client voulait pas vraiment être sur que la surface disponible dans un immeuble était égale à la somme des surface des appartements. Dans le cas d’un client honnête, si il recherche à maintenir cette propriété, il est possible de vérifier que le programme garantit qu’un employé ne va pas aller tricher avec les données en bidouillant n’importe comment.
Le « modèle métier » c’est plutôt le modèle qui va te dire qu’un avion a en général deux ailes chez Airbus, ou que le débit et le crédit d’un compte bancaire doivent s’équilibrer chez un comptable.
Et c’est indépendant de la correction du compilateur, vu que c’est la cohérence «interne». La correction du compilateur garantit que ces propriétés seront préservées par la compilation.
[^] # Re: Le cerveau n'est pas logique
Posté par Thomas Douillard . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Moué, ça se voit la que tu racontes n’imp.
[^] # Re: Le cerveau n'est pas logique
Posté par Thomas Douillard . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
La logique peut aussi vérifier la cohérence interne des connaissances des experts sur leur sujet. Mais effectivement elle va pas créer ex nihilo le modèle métier ou une théorie scientifique. Ça mettrai un paquet d’universitaires et d’informaticiens au chomage :) Mais du point de vue de la cohérence, ça peut lever des lièvres.
[^] # Re: Intérêt ?
Posté par Thomas Douillard . En réponse au journal Tous les parsers JSON sont mauvais. Évalué à 10. Dernière modification le 24 octobre 2017 à 11:54.
D’une manière générale, dire « aucune limite » c’est un raccourcis pour dire « toute la mémoire dispo ». En vrai, ça finira toujours par planter pour certains niveau d’imbrications - si c’est pas la pile qui explose, ce sera le tas. Si c’est pas le tas, ça sera le dd si t’as été pervers au point d’utiliser un fichier pour compter les accolades. Ça donne un fichier suffisamment grand pour toutes les applications réalistes, mais qui existe tout de même.
Et puis si t’en es à devoir traiter un arbre très très profond - alors que tout le point d’un arbre c’est en général de maintenir un certain niveau d’horizontalité et d’éviter de partir en profondeur (un index typiquement, que tu essayes de maintenir équilibré) t’as probablement d’autres préoccupations. Un arbres très profond, si on le suppose équilibré, ça veut dire que la taille des donnée est exponentiellement plus grande, donc absolument gigantesque. Peu de chances que ça termine dans un fichier json, en somme.
[^] # Re: Possibilité d'éditer ses propres contenus
Posté par Thomas Douillard . En réponse à la dépêche Améliorons l’expérience utilisateur de LinuxFr.org !. Évalué à 1.
Et une culture chez certains contributeurs vis à vis de la sécurité je pense. Avec une idée « le seul moyen de corriger une faille c’est de l’exploiter » qui incite a des comportements complètement non naturels genre des comptes problématiques qui apparaissent opportunément pour troller. Ça incite à des postures excessivement défensives. Genre par crainte de de comportement détester jouer une caricature à la puissance 10 dudit comportement afin de pousser à l’interdire.
[^] # Re: go 2.0
Posté par Thomas Douillard . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
J’ajouterai perso que la théorie sur la sémantique d’un langage, ça devrait largement aider à construire un outillage puissant pour l’écosystème du langage.
L’exemple de l’inférence de type est un cas d’école, je pense : c’est une fonctionnalité très bien comprise théoriquement, qui permet d’aider le programmeur à faire moins d’erreur. La coloration syntaxique, c’est quand même utile d’avoir une grammaire formelle pour l’implémenter, et ces objets sont très bien connus théoriquement. Ça fait partie du baggage de base d’un informaticien. Peut être d’ailleurs qu’un des boulot du chercheur en langage c’est d’essayer de penser à des outils que la formalisation des langages peut aider à concevoir … après tout si c’est plus régulier et plus compréhensible pour les humains, c’est aussi très utile pour les machines pour raisonner sur le programme …
[^] # Re: Super texte …
Posté par Thomas Douillard . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2. Dernière modification le 18 octobre 2017 à 19:47.
Ah oui pardon, j’ai dû être trompé par « Dans cette partie du texte, quand je parle de "voir un programme comme un objet mathématique", je parle plutôt du code source ». Toujours cette satanée confusion … c’est absolument pas naturel pour moi de considérer le code simplement comme un programme.
On est pas aidé par des expressions comme langage formel. En fait un langage de programmation (ou sa formalisation) est du côté des système formels, un langage formel en fait simplement partie. Le système formel est constitué du couple (langage formel, sémantique), et on est d’accord que la grammaire définit la partie « langage formel ».
[^] # Re: Super texte …
Posté par Thomas Douillard . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Ça se discute. Tu notes une relation de temporalité (voire de causalité) qui n’existe pas forcément dans le monde mathématiques. On ne définit pas les entiers en donnant tous les exemples d’entiers, et une fois qu’on l’a fait, on définit les entiers. On donne des axiomes qui permettent de décider si un objet du formalisme est ou pas un entier. Par l’axiome d’extensionnalité, à tout prédicat correspond une extension : « Étant donné un ensemble A et une propriété P exprimée dans le langage de la théorie des ensembles, il affirme l'existence de l'ensemble B des éléments de A vérifiant la propriété P » https://fr.wikipedia.org/wiki/Sch%C3%A9ma_d%27axiomes_de_compr%C3%A9hension . Mais à chaque propriété sur un ensemble correspond une seule extension … que tu définis « en même temps » que tu donnes la propriété. En complexité, on définit même un problème de décision comme l’appartenance ou pas d’une chaîne à un ensemble. Le prédicat associé à l’ensemble n’est même pas évoqué … En gros dans mon esprit la BNF (le prédicat) définit l’ensemble (le langage). Sauf si tu assimiles l’écriture de la BNF à la définition d’«un» programme, mais c’est pas du tout ma vision des choses. Enfin cette manière de décrire les choses correspond peut être à une vision constructiviste des choses ;).
Sinon je suis entièrement d’accord pour ce que tu dis sur la formalisation, avoir un accord parfait entre la théorie et l’expérience est un acte inaccessible. Cela dit, je pense avoir identifié un truc qui manque dans ton texte : il est considéré comme implicite que le programme est destiné à être exécuté. Du coup la métaphore du « parler » tombe un peu à plat. Quand je fais une requête google, je « parle » à la machine, pourtant je ne la programme pas. Un programme est destiné à être exécuté, et peut être exécuté pleins de fois. ça ne transparaît dans ton texte que quand tu parles de comportement du programme. Ce qui pourrait lever ton ambiguïté d’ailleurs.
(et je poste en l’état parce que j’y ai déjà passé trop de temps)
[^] # Re: Super texte …
Posté par Thomas Douillard . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Je dirai que « les informaticiens ont inventé de nombreuses manières de décrire les programmes qui sont exécutés par un ordinateur » conviendrai dans un premier temps. Tu peux rajouter « souvent ils sont écris sous forme de texte, parfois d’autres formes, ou d’autres formes symboliques (« graphiques » par ex. https://scratch.mit.edu/) ». Dans tous les cas, le formalisme qui permet de les décrire constitue ce qu’on appelle un « langage de programmation ». »
Je comprend pas. Un programme écrit dans un langage donné est quelque part déjà un objet mathématique. « et à partir de cela définir le langage » euh, on commence pas par définir le langage avant d’écrire des programmes ??? Peut être qu’il faut que tu parles de sémantique (en général) d’un langage de programmation, sinon pareil je pense que ça peut ne pas être clair pour un débutant.
Je propose :
«Les informaticiens apprennent souvent par l’exemple et la pratique (et un prof et ses explications) ce qu’est supposé faire un programme et se forgent une intuition de la signification du code qu’ils écrivent, Ensuite, on essaye de le faire tourner pour voir si « ça marche » … et parfois, « ça marche ».
Les approches formelles s’appuient sur autre choses que l’essai et l’erreur et s’appuient sur la logique et les mathématiques pour décrire le comportement attendu d’un programme (indépendamment de ce qui se passe vraiment quand on le teste). La sémantique formelle (cette fois) d’un langage permet de faire le lien entre chaque programme écrit dans ce langage et ce comportement attendu. Votre boulot est en partie de l’écrire et de l’imaginer.»
Du coup vous vous nourrissez de la rigueur des maths pour détecter d’éventuels problèmes, et le point de vue différent offert peut donner de nouvelles idées et définir des choses précises là ou les langages de programmation « défini par l’implémentation ou la doc » sont moins précis et solides, peuvent avoir des trous et des points non documentés ou on est vraiment obligé de tester pour savoir ce que ça fait « en vrai ». Non ?
« Intuitivement on pense à le définir comme un ensemble de programmes » Mmm certainement pas l’intuition d’un débutant … En fait ce que tu entend par « programme » n’est pas forcément clair. Et cette intuition de programme en tant que composition de programme interroge sur une notion de « programme primitif » qui est un peu HS et pas du tout intuitive pour quelqu’un qui ne connait pas la programmation. C’est un peu une impasse, je pense.
J’imagine que par « mathématiquement » tu veux dire « dans un formalisme logique ».
Il faut que tu utilises soit un langage algorithmique basique, qu’on peu facilement assimiler à un langage de programmation, soit des formules déclaratives (dans une logique) pour décrire des propriétés du résultats. La preuve visera à démontrer que les opérations décrites par l’algo réalisent bien les propriétés attendues. Ton utilisation de « mathématique » me gène en fait, en tant que personne qui connait un peu le domaine.
Autre remarque :
Je pense que c’est clair uniquement pour ceux qui savent ce qu’est une relation mathématique.
[^] # Re: J'aime les arbres
Posté par Thomas Douillard . En réponse au sondage Que pensez-vous des liseuses ?. Évalué à 4.
Ça n’absorbe pas grand chose si le papier finit cramé. Le CO2 est relargué relativement rapidement. Au mieux le bilan carbone de la filière est neutre si ces bois produisent suffisamment de matière pour l’industrie du papier, et en ignorant les énergies nécessaires au transport et à la fabrication du papier.
En plus pour des bouquins qui seront lus souvent une fois ou resteront invendus et termineront direct au pilon et au recyclage … voire prendront de la place et de la poussière dans une bibliothèque.
Cela dit j’aime bien le support papier, mais c’est pas ces forets d’exploitation qui vont le sauver. Le bilan d’une liseuse est probablement désastreux aussi, mais c’est sans doute mieux pour la forêt et la biodiversité en général. Petite pensée opur tous les auteurs qui ne sont pas Amélie Nothomb et qui peinent à se faire éditer aussi.
# Super texte …
Posté par Thomas Douillard . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Je trouve ça dans l’ensemble très clair et très intéressant, même en étant pas la cible. Après je pense que la première phrase est un peu sèche pour un béotien (« représentation symbolique », ça peut faire peur, ce serait dommage). Et tu ne reparles pas de symbole dans la suite, donc l’utilité est sans doute discutable.
Quelques remarques :
Je pense aussi que tu peux intervertir « formalisation mathématique d'un langage de programmation » et « sémantique formelle ». Le second est plus technique, utiliser la première expression en définissant la seconde.
Un peu ambigu je trouve, mais c’est pas très grave, et peut être un peu confusant : le programme peut être considéré comme la spécification d’un algorithme dans un langage, alors que la sémantique formelle peut être considérée comme la spec du langage lui même. Ou alors tu veux dire que si le langage n’a pas de sémantique formelle, on ne peut pas considérer le programme comme un objet mathématique ? Mais je pinaille peut être un peu beaucoup pour ce que tu cherches à faire.
[^] # Re: XMPP, Pas facile de s'y retrouver
Posté par Thomas Douillard . En réponse à la dépêche Sortie du très attendu Prosody 0.10. Évalué à 4.
Tu entends quoi par "de plus en plus buggué" ? C'est étrange car encore maintenu.
# Débattons !
Posté par Thomas Douillard . En réponse à la dépêche Le développement de « Débattons » est lancé !. Évalué à 7.
J'espère que vous allez mettre débattons sur les rails, et pas dans les roues !
[^] # Re: Trollons
Posté par Thomas Douillard . En réponse à la dépêche Le développement de « Débattons » est lancé !. Évalué à 4.
Alors que je suis juste tombé sur un nid de gens contre le progrès sur Internet blasés !
[^] # Re: Trollons
Posté par Thomas Douillard . En réponse à la dépêche Le développement de « Débattons » est lancé !. Évalué à 2.
L’idée c’est de débattre et de supprimer les silos, donc c’est fort possible. C’est presque le but. Mais l’idée ça a aussi l’air de pas refaire 43 milles fois le match, genre comme c’est possible en relançant un thread sur linuxfr ou tu vas dupliquer la même discussion.
Donc les farfelus, tout l’enjeu technique est de fournir des moyens de leur faire comprendre que le match à déjà eu lieux et que les arguments on déjà été donnés.
[^] # Re: XMPP, Pas facile de s'y retrouver
Posté par Thomas Douillard . En réponse à la dépêche Sortie du très attendu Prosody 0.10. Évalué à 9.
Je sais que ce n'est pas du tout ton objectif principal, mais si tu arrétais de personnaloser les débats àtpjt bout de champ ce serait quand même une bonne chose pour l'ambiance.
# Resumé
Posté par Thomas Douillard . En réponse à la dépêche Le développement de « Débattons » est lancé !. Évalué à 4.
Vous avez connaissance de systèmes de résumé comme wikum ? Cf. https://linuxfr.org/users/thoasm/journaux/wikum-resume-et-recursion ca me semble intéressant à considérer pour une telle plateforme.
[^] # Re: Trollons
Posté par Thomas Douillard . En réponse à la dépêche Le développement de « Débattons » est lancé !. Évalué à 3.
J'ai l'impression que c'est précisément ce qu'ils cherchent à éviter.
[^] # Re: du boulot!
Posté par Thomas Douillard . En réponse au journal Wikum : Résumé et récursion. Évalué à 4.
Il ne suffit pas de ne pas permettre des commentaires de résumé ?
Dans le papier il notent le fait qu’on note un début de «culture» du résumé avec les pratiques des participants qui s’alignent sur les pratiques des premier contributeurs du résumé, ça note que la communauté adopte une position pragmatique. Je pense que cette «culture» peut se bonifier avec l’expérience, et je pense aussi qu’elle se baserai sur l’intérêt communautaire bien compris (faire un résumé utile), et pas sur une volonté de discuter chaque virgule. En particulier, sur ce que tu dis, je pense qu’il s’agit de dépersonnaliser les arguments (ne pas évoquer « machin »), et mentionner le problème en question et ne pas le qualifier
Dans cette approche, j’ai l’impression que l’utilité est aussi de servir de « poteau indicateur » et de jouer le rôle de « sommaire » de la discussion.