Ah ouais, en lisant les posts de blogs ça sent l’amateurisme dans l’implémentation du langage. Des programmes vala qui marchent pas parce que le C généré n’est pas du C c’est quand même pas terribles.
C'est un indicateur, un moyen intermédiaire pour remplir des objectifs plus ambitieux (diminuer le chômage, améliorer le niveau de vie).
… pfff fastidieux comme discussion. Je crois effectivement qu’on est pas sur la même longueur d’onde. La variation du PIB est tellement associé à « vivre mieux » et les politiques ont tellement les yeux rivés sur cet indicateur qu’en pratique j’ai aucun scrupule à ne pas considérer que ton analyse contredit la mienne.
Croitre le PIB est une condition nécessaire pour vivre mieux. Là est le dogme. En pratique, quand on remplace les abeille par des humains pour polliniser parce qu’il n’y a plus d’abeille, on a diminué le chômage. Pas sur que quiconque vive mieux pour autant. Pas de quoi remettre quoi que ce soit en cause pour autant dans le système économique et sa gestion.
Ouais alors t’as raté que « croissance » c’est … croissant. Donc ça monte. C’est pas neutre. On appellerait ça « niveau de richesse » ce serait quelque chose. Mais non. C,est la croissance du niveau de richesse que ça signifie.
Quand on parle d’un indicateur neutre, genre la population, on fait un recensement et on dit « il y a tant de personne dans le pays ». Mais ça fait un moment que la croissance de la population n’est plus un objectif politique.
Faut pas tout mélanger, la croissance, c’est pas l’économie c’est un objectif politique.
C’est basé sur la croyance que cet objectif maximise le bien commun. Après, sachant que les économistes sont quand même subordonnés à des choix politiques, la croissance est un élément central des modèles économiques, qui peut s’étudier de manière scientifique.
L’erreur serait de croire que c’est le seul paradigme possible pour l’économie … Mais tant que le politique ne poursuivra que cet objectif, ce sera dur d’avoir des données sur l’économie dans ces politiques différentes. Je pense qu’un terme plus correct que dogme serait « paradigme ». Le problème principal de la science économique, c’est que le changement de paradigme scientifique dépend assez largement du changement de paradigme politique … et c’est pas une mince affaire de faire bouger les lignes politiques.
Je force volontairement le trait de la distinction, parce que le fait qu’il existe des relations incestueuses entre économie politique et scientifique brouille complètement les lignes. C’est la vraie difficulté pour l’économie en tant que science.
Pour que les comportements indéfinis du C/C++ ne soient pas un problèmes, il ne faut pas apprendre la spec par cœur. Suffit de programmer en utilisant d’autres langages.
Et figure toi que ça n’implique pas d’âtre un mauvais programmeur ;)
Attention, bientôt tu vas exiger un permis de programmer comme d’autres veulent un permis d’utiliser un ordinateur. Le soucis c’est qu’on risquerait de se retrouver facilement avec une pénurie de programmeur avec ce niveau d’exigence.
Ici tu confonds deux choses : la logique du premier et la logique intuitionniste. La première concerne les règles de formation des jugements, la seconde traite des règles d'inférences ou raisonnements.
Mmm après réflexion je dirai plutôt que je fais une erreur stupide : je confonds implication et déduction. Par définition, une logique s’intéresse aux règles de constructions et à la formation des jugements … 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 … Je crois que tu confonds « formule de la logique du premier ordre » et « logique du premier ordre ». Ou alors c’est moi qui confond … Parce que dans mon esprit, la logique du premier ordre est un système formel, donc comprend les règles de déduction : https://en.wikipedia.org/wiki/First-order_logic (et wp semble être d’accord avec moi) ou alors j’ai rien compris à ce que tu dis :) La logique intuitionniste est aussi un système de déduction, mais avec des règles de déduction différente. Ou alors tu voulais dire « la logique intuitionniste du premier ordre est l’archétype du typage dynamique » ?
Du coup je me fourvoyai effectivement, tu parlais à chaque fois de système de déduction intuitionnistes. Tu établis 'une correspondance preuve/programme qui ne fonctionne que pour ces système, et je pensai que tu associais un système non intuitionniste pour les langages dynamiques. Alors que tu établies plus une distinction théorie à variable typée/théorie à variable pas typée.
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.
Sinon t’embêtes pas trop sur le Kantisme, j’ai parcouru les articles sur « noumène et phénomène » de la wp en anglais, qui sont instructifs et mettent bien en lumière les difficultés d’interprétation. , j’en conclu que tout tourne autour du thème « la réalité est-elle concevable », « peut-on concevoir l’inconcevable » (peut-on nommer l’innommable). Ça me semble un peu une tentative de formalisation du problème de la recherche scientifique. (est-ce qu’on peut trouver ce qu’on cherche pas?) Est-ce qu’on peux spécifier la totalité de la réalité ?
Du coup, on peut se demander si ce n’est pas voué à l’échec. Toute formulation de ce problème est voué à s’enfermer dans son propre cadre théorique. D’une part, effectivement il est trivial qu’on a accès qu’à l’univers observable en l’état des connaissances actuelles. D’autre part, cette formalisation elle même, si on prend la réciproque de ta propre affirmation que tout ce qui est entendable ou logique peut s’exprimer en langage naturel, peut s’exprimer dans une logique.
Et là, on tombe sur des considérations Godelienne :) dans quelle mesure peut-on affirmer que l’axiomatique induite par cette formalisation est cohérente, ou indépassable ? Si elle est cohérente, elle est incomplète, et donc dépassable ? Ça ne contredirait pas un peu la transcendance de cette vision des choses ?
Tu prends là une condition suffisante (l'existence propre de l'objet expliquerait l'accord des observateurs), pour une condition nécessaire (leur accord ne peut s'expliquer que par une existence propre de l'objet, abstraction faite du rapport à l'observateur)
Il n’y a pas grand chose de ni nécessaire, ni suffisant dans l’accord entre observateurs pour montrer grand chose. L’observation est faillible par essence, et deux observateurs peuvent faillir de la même manière. On ne peux que constater que la méthode scientifique finit par générer quelque chose qui ressemble à un accord. Ce qui en soit est considéré comme une quasi religion pour Eintein ;) Et ce en tentant aux maximum de s’affranchir de nos biais et illusions en multipliant les méthodes d’observation. Cela dit si tu ne postules pas ça, il ne peux y avoir de sciences.
parler d'observation sans observateur (c'est-à-dire en faisant abstraction du rapport entre l'observateur et l'objet observé) est une contradiction dans les termes.
Je comprends pas trop en quoi tu postules que je veux me débarrasser de l’observateur. Il me semble assez naturel aussi de postuler que nos théories ne sont pas la réalité. A partir de là on peut déduire que l’homme, en tant qu’être doué de raison, tente juste de déceler l’ordre dans le monde en vue de le prévoir. Il réussit, ou il échoue ;)
Premièrement, l'accord entre observateurs sur les determinations spatio-temporelles des objets est tout sauf commun : voir les principes fondamentaux des relativité restreinte et générale.
L’accord entre observateurs existe aussi en relativité générale, je trouve ça assez moyen comme contre exemple. Il est simplement plus compliqué à établir, car il faut utiliser les équations de changements de référentiels prévus par la théorie. Il passe par ce proxy pour éviter ce qui pourrait sembler absurde à l’observateur humain naïf plongé prêt d’un trou noir ou en voyage spatial.
dans la connaissance expérimentale on ne pose jamais de questions sur ce que sont les choses en elles-même, mais seulement sur les résultats de nos observations;
Bien sur que si, il est impossible de concevoir une expérience scientifique un tant soit peu élaborée sans se poser des questions sur la nature de l’objet observé. Il est par exemple impossible de mesurer un quelconque spin d’une particule sans avoir postulé qu’il devait exister une telle quantité, ou qu’elle représentai quelque chose. Alors évidemment ça ne veut pas dire qu’on a une réponse absolue sur la nature de la chose qu,on veut observer, mais on a au moins l’idée (ou l_’espoir) que faire une telle expérience a un sens. Nos théorie ont pour vocation de nous renseigner sur la nature des choses. Ça implique nécessairement la question de la théorisation, qui est une étape loin d’être triviale à partir des observations. La relativité générale permet de restaurer l’accord
Je vois alors l'énoncé comme une fonction qui prend en entrée un interface{} et qui fait du typage dynamique : une assertion de type ou un switch (comme tu veux), comme en Go.
Je comprend bien l’idée, mais l’analogie trouve ses limites vu que la logique du premier ordre n’est pas constructive. Si x n’appartient pas à Oméga, ben, rien, ça ne pose pas de problème. Donc « exécution » n’a pas trop de sens. Par contraste, en python, si tu passes un objet d’un mauvais type à une fonction, ben « boom ». Python se comportera pas bien du tout … Alors que dans une implication logique, un ensemble qui ne vérifie pas la prémisse ne sera jamais susceptible de fournir un contre exemple de l’implication.
La notion de type capture bien mieux que celle d'ensembles (au sens de ZF) la notion logique de concept.
Je te suis pas. C’est une notion logique la notion de concept ?
ce ne sont que de simples phénomènes qui n'ont pas d'existence propre en dehors de leur rapport à un observateur.
Le truc qui me choque à chaque fois que je croise ce genre de philosophie : et quand il y a 2 observateurs ? Et que par hasard ils sont d’accord, ce qui n’est pas systématique, mais assez commun. On peut donc arguer qu’ils tirent les mêmes conclusions sur l’objet en question, ce qui tend à montrer que ces phénomènes ont une existence propre. On ne cherche pas autre chose que nous rassurer sur la pertinence de nos observations en sciences en tentant de rendre les résultats reproductibles.
ZF c'est l'archétype du typage dynamique
Je suis intéressé par une explication là dessus. ZF est bien fondée dans le sens ou toute compréhension est associée à un ensemble préexistant https://fr.wikipedia.org/wiki/Sch%C3%A9ma_d%27axiomes_de_compr%C3%A9hension « É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. » ce que j’interprète (librement) comme une relation de sous typage. Étant donné que le « x ∈ A » ressemble quand même pas mal à une assertion de type et qu’elle est nécessaire dans une théorie des ensemble, j’ai du mal à comprendre en quel sens ça correspond à un langage dynamique.
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.
[^] # Re: Vala
Posté par thoasm . En réponse au journal Peek, capture d'écran au plus simple. Évalué à 4.
Ah ouais, en lisant les posts de blogs ça sent l’amateurisme dans l’implémentation du langage. Des programmes vala qui marchent pas parce que le C généré n’est pas du C c’est quand même pas terribles.
C’est ptete pas un langage très intéressant du point de vue théorique mais c’est peut être un cas d’étude intéressant pour nos experts en langages locaux https://linuxfr.org/users/bluestorm/journaux/pourquoi-la-recherche-en-langages-de-programmation
[^] # Re: La gouvernance par les nombres
Posté par thoasm . En réponse au journal ils l'ont voulu, ils l'ont obtenu, et ils l'ont dans le baba.... Évalué à 9.
… pfff fastidieux comme discussion. Je crois effectivement qu’on est pas sur la même longueur d’onde. La variation du PIB est tellement associé à « vivre mieux » et les politiques ont tellement les yeux rivés sur cet indicateur qu’en pratique j’ai aucun scrupule à ne pas considérer que ton analyse contredit la mienne.
Croitre le PIB est une condition nécessaire pour vivre mieux. Là est le dogme. En pratique, quand on remplace les abeille par des humains pour polliniser parce qu’il n’y a plus d’abeille, on a diminué le chômage. Pas sur que quiconque vive mieux pour autant. Pas de quoi remettre quoi que ce soit en cause pour autant dans le système économique et sa gestion.
[^] # Re: La gouvernance par les nombres
Posté par thoasm . En réponse au journal ils l'ont voulu, ils l'ont obtenu, et ils l'ont dans le baba.... Évalué à 2.
Ouais alors t’as raté que « croissance » c’est … croissant. Donc ça monte. C’est pas neutre. On appellerait ça « niveau de richesse » ce serait quelque chose. Mais non. C,est la croissance du niveau de richesse que ça signifie.
Quand on parle d’un indicateur neutre, genre la population, on fait un recensement et on dit « il y a tant de personne dans le pays ». Mais ça fait un moment que la croissance de la population n’est plus un objectif politique.
[^] # Re: La gouvernance par les nombres
Posté par thoasm . En réponse au journal ils l'ont voulu, ils l'ont obtenu, et ils l'ont dans le baba.... Évalué à 8.
Faut pas tout mélanger, la croissance, c’est pas l’économie c’est un objectif politique.
C’est basé sur la croyance que cet objectif maximise le bien commun. Après, sachant que les économistes sont quand même subordonnés à des choix politiques, la croissance est un élément central des modèles économiques, qui peut s’étudier de manière scientifique.
L’erreur serait de croire que c’est le seul paradigme possible pour l’économie … Mais tant que le politique ne poursuivra que cet objectif, ce sera dur d’avoir des données sur l’économie dans ces politiques différentes. Je pense qu’un terme plus correct que dogme serait « paradigme ». Le problème principal de la science économique, c’est que le changement de paradigme scientifique dépend assez largement du changement de paradigme politique … et c’est pas une mince affaire de faire bouger les lignes politiques.
Je force volontairement le trait de la distinction, parce que le fait qu’il existe des relations incestueuses entre économie politique et scientifique brouille complètement les lignes. C’est la vraie difficulté pour l’économie en tant que science.
[^] # Re: N'utilife pluf lef icônef du thème GTK
Posté par thoasm . En réponse au journal Le Firefox nouveau est arrivé !. Évalué à 2.
Tentative de troll sur l’esthétique de la langue ? ça a vaguement démarré sur le dernier journal sur l’écriture inclusive.
[^] # Re: Le cauchemar de Trougon
Posté par thoasm . En réponse au journal Le cauchemar d'Henry. Évalué à 1.
Mais non, tu t’es réveillé dans un « escape room ».
[^] # Re: Jean-François Revel commente ainsi la féminisation des mots
Posté par thoasm . En réponse au journal Partage. Évalué à -2.
c’est quoi la langue officielle ?
[^] # Re: Jean-François Revel commente ainsi la féminisation des mots
Posté par thoasm . En réponse au journal Partage. Évalué à 4.
J'aurai tendance à répondre, si on s'en fiche tant que ça de cet arbitraire sans aucun sens, on se fiche un peu de changer la règle du jeu.
[^] # Re: Comportement indéfini ou incorrect ?
Posté par thoasm . En réponse au journal Compilateur trop intelligent. Évalué à 7.
C’est une variable statique. Donc si j’ai la bonne ligne dans la spec : https://port70.net/~nsz/c/c11/n1570.html#6.7.9p10
[^] # Re: Utilisateur trop bête
Posté par thoasm . En réponse au journal Compilateur trop intelligent. Évalué à 1.
Pour que les comportements indéfinis du C/C++ ne soient pas un problèmes, il ne faut pas apprendre la spec par cœur. Suffit de programmer en utilisant d’autres langages.
Et figure toi que ça n’implique pas d’âtre un mauvais programmeur ;)
[^] # Re: Utilisateur trop bête
Posté par thoasm . En réponse au journal Compilateur trop intelligent. Évalué à 4.
Attention, bientôt tu vas exiger un permis de programmer comme d’autres veulent un permis d’utiliser un ordinateur. Le soucis c’est qu’on risquerait de se retrouver facilement avec une pénurie de programmeur avec ce niveau d’exigence.
[^] # Re: copie efficace vers/de une machine distante
Posté par thoasm . En réponse à la dépêche Sortie de gfast-copy et de fast-copy sur www.open-source-projects.net. Évalué à 5.
Bug rapporté ?
[^] # Re: Le cerveau n'est pas logique
Posté par thoasm . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Mmm après réflexion je dirai plutôt que je fais une erreur stupide : je confonds implication et déduction. Par définition, une logique s’intéresse aux règles de constructions et à la formation des jugements … 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 … Je crois que tu confonds « formule de la logique du premier ordre » et « logique du premier ordre ». Ou alors c’est moi qui confond … Parce que dans mon esprit, la logique du premier ordre est un système formel, donc comprend les règles de déduction : https://en.wikipedia.org/wiki/First-order_logic (et wp semble être d’accord avec moi) ou alors j’ai rien compris à ce que tu dis :) La logique intuitionniste est aussi un système de déduction, mais avec des règles de déduction différente. Ou alors tu voulais dire « la logique intuitionniste du premier ordre est l’archétype du typage dynamique » ?
Du coup je me fourvoyai effectivement, tu parlais à chaque fois de système de déduction intuitionnistes. Tu établis 'une correspondance preuve/programme qui ne fonctionne que pour ces système, et je pensai que tu associais un système non intuitionniste pour les langages dynamiques. Alors que tu établies plus une distinction théorie à variable typée/théorie à variable pas typée.
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.
[^] # Re: Le cerveau n'est pas logique
Posté par thoasm . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
Sinon t’embêtes pas trop sur le Kantisme, j’ai parcouru les articles sur « noumène et phénomène » de la wp en anglais, qui sont instructifs et mettent bien en lumière les difficultés d’interprétation. , j’en conclu que tout tourne autour du thème « la réalité est-elle concevable », « peut-on concevoir l’inconcevable » (peut-on nommer l’innommable). Ça me semble un peu une tentative de formalisation du problème de la recherche scientifique. (est-ce qu’on peut trouver ce qu’on cherche pas?) Est-ce qu’on peux spécifier la totalité de la réalité ?
Du coup, on peut se demander si ce n’est pas voué à l’échec. Toute formulation de ce problème est voué à s’enfermer dans son propre cadre théorique. D’une part, effectivement il est trivial qu’on a accès qu’à l’univers observable en l’état des connaissances actuelles. D’autre part, cette formalisation elle même, si on prend la réciproque de ta propre affirmation que tout ce qui est entendable ou logique peut s’exprimer en langage naturel, peut s’exprimer dans une logique.
Et là, on tombe sur des considérations Godelienne :) dans quelle mesure peut-on affirmer que l’axiomatique induite par cette formalisation est cohérente, ou indépassable ? Si elle est cohérente, elle est incomplète, et donc dépassable ? Ça ne contredirait pas un peu la transcendance de cette vision des choses ?
[^] # Re: Le cerveau n'est pas logique
Posté par thoasm . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
Il n’y a pas grand chose de ni nécessaire, ni suffisant dans l’accord entre observateurs pour montrer grand chose. L’observation est faillible par essence, et deux observateurs peuvent faillir de la même manière. On ne peux que constater que la méthode scientifique finit par générer quelque chose qui ressemble à un accord. Ce qui en soit est considéré comme une quasi religion pour Eintein ;) Et ce en tentant aux maximum de s’affranchir de nos biais et illusions en multipliant les méthodes d’observation. Cela dit si tu ne postules pas ça, il ne peux y avoir de sciences.
Je comprends pas trop en quoi tu postules que je veux me débarrasser de l’observateur. Il me semble assez naturel aussi de postuler que nos théories ne sont pas la réalité. A partir de là on peut déduire que l’homme, en tant qu’être doué de raison, tente juste de déceler l’ordre dans le monde en vue de le prévoir. Il réussit, ou il échoue ;)
Bien sur que si, il est impossible de concevoir une expérience scientifique un tant soit peu élaborée sans se poser des questions sur la nature de l’objet observé. Il est par exemple impossible de mesurer un quelconque spin d’une particule sans avoir postulé qu’il devait exister une telle quantité, ou qu’elle représentai quelque chose. Alors évidemment ça ne veut pas dire qu’on a une réponse absolue sur la nature de la chose qu,on veut observer, mais on a au moins l’idée (ou l_’espoir) que faire une telle expérience a un sens. Nos théorie ont pour vocation de nous renseigner sur la nature des choses. Ça implique nécessairement la question de la théorisation, qui est une étape loin d’être triviale à partir des observations. La relativité générale permet de restaurer l’accord
Je comprend bien l’idée, mais l’analogie trouve ses limites vu que la logique du premier ordre n’est pas constructive. Si x n’appartient pas à Oméga, ben, rien, ça ne pose pas de problème. Donc « exécution » n’a pas trop de sens. Par contraste, en python, si tu passes un objet d’un mauvais type à une fonction, ben « boom ». Python se comportera pas bien du tout … Alors que dans une implication logique, un ensemble qui ne vérifie pas la prémisse ne sera jamais susceptible de fournir un contre exemple de l’implication.
[^] # Re: Le cerveau n'est pas logique
Posté par thoasm . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
Le truc qui me choque à chaque fois que je croise ce genre de philosophie : et quand il y a 2 observateurs ? Et que par hasard ils sont d’accord, ce qui n’est pas systématique, mais assez commun. On peut donc arguer qu’ils tirent les mêmes conclusions sur l’objet en question, ce qui tend à montrer que ces phénomènes ont une existence propre. On ne cherche pas autre chose que nous rassurer sur la pertinence de nos observations en sciences en tentant de rendre les résultats reproductibles.
[^] # Re: Le cerveau n'est pas logique
Posté par thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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.