kantien a écrit 1248 commentaires

Justement, tu précises « sécurité mémoire »

Et c'est ce que prétend apporter, à raison, le langage Rust. Il n'a jamais prétendu être la panacée contre tous les types de bugs. L'erreur du unwrap peut se reproduire dans les autres langages, mais leurs bugs mémoires n'ont pas d'équivalents en Rust.

Ceux qui cherchent à troller Rust inventent un adversaire imaginaire : ils combattent un homme de paille.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'ai vu ma sœur ce week-end, et j'ai un peu plus d'infos. Elle n'est pas sur le dossier de la Pascaline donc ne connaît pas tous les détails. Dans l'ensemble, elle a trouvé que tu as avais bien cerné les problématiques qu'ils se posent sur la conservation en général.

Sur le sujet de la Pascaline, ils en ont déjà trois. Alors, certes, ils n'ont pas ce modèle mais elles sont toutes sur le même principe. Dans l'absolu, avec un budget d'acquisition illimité (le leur est ridiculement bas), elle a certes un intérêt patrimonial mais c'est juste de la bonne horlogerie faite de la main de Pascal. Les pascalines ont aussi des « bugs », leur sautoir s'use avec le temps ce qui exige de devoir la règler pour assurer son bon fonctionnement.

Ils ont néanmoins dans leur collection des objets dont l'intérêt réside dans la composition de la matière qui les constitue. Elle m'a donné l'exemple du Buste Deville fait dans un aluminium produit par des procédés chimique, il est « l’un des rares témoins de la production en aluminium antérieure à 1886, date à laquelle la voie chimique est supplantée par un procédé électrolytique beaucoup plus rentable qui donnera enfin des débouchés industriels au métal de l’argile ».

Après ils leur arrivent aussi de détruire des objets qu'il serait trop coûteux de conserver. Comme la Numasurf, un fraiseuse qui témoigne des débuts de la conception assistée par ordinateur, utilisée chez Renault. Ils ont conservé la tête de fraisage, des tonnes de documentation, le logiciel… mais envoyé le reste de la machine à la benne. Néanmoins, ils ont auparavant procédé à une numérisation 3D complète de la machine afin de la réstituer dans un environnement de réalité virtuelle.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'ai oublié, panic c'est la règle d'élimination de l'absurde : le programmeur est tombé sur une contradiction, et au lieu de chercher à la comprendre, pour proposer une solution, il a paniqué. ;-)

Pour pouvoir valider le type de unwrap, il faut que panic produise le type T que l'on a en cas de succès, quelque soit le type E des erreurs. Le type de panic produit le type qu'il veut en sortie quelque soit son type d'entrée, c'est à dire l'élimination de l'absurde ou le principe ex falso quodlibet (du faux, fait ce qu'il te plait).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

les cRUSTacés vont t’expliquer que malgré les bogues qu’ils créent ils sont automagiquement plus sûr parce-que c’est comme ça

Et pourtant, ils le sont (plus sûrs) !

Là, c'est un exemple typique de ce que j'expliquais quand je disais que les programmeurs faisaient de l'axiomatique sans le savoir (API, c'est Axiomatique Pour Informaticien).

Le type Result <T,E> est l'équivalent logique d'une disjonction : on a un résultat de type T ou une erreur de type E. L'axiomatique minimale et complète pour ce type est celle-ci :

val ok : 't -> ('t,'e) Result
val error : 'e -> ('t, 'e) Result
val fold : ('ok -> 'res) -> ('err -> 'res) -> ('ok, 'err) Result -> 'res

J'ai utilisé la syntaxe OCaml que je maîtrise mieux. Mais l'idée est qu'avec seulement ces 3 fonctions on peut implémenter toute l'API du type Result. Par exemple, le trait unwrap incriminé s'implémente ainsi :

unwrap self = fold id panic self

où id est la fonction identité qui renvoie son argument et panic c'est ce qui est arrivé en cas d'erreur.

Que ces trois fonctions suffisent, on le doit à Gödel (théorème de complétude) et Gentzen (déduction naturelle). Le type de ces trois fonctions correspondent aux règles de la déduction naturelle pour la disjonction : les deux premières sont les règles d'introduction de la disjonction (comment produire un Result) et la troisième à la règle d'élimination (comment consommer un Result).

Ce qu'il y a, c'est que unwrap, qui de fait appel panic, ne doit être utiliser que sur des erreurs irrécupérables ! Il est peu probable que ce soit le cas ici, et unwrap n'aurait jamais du se trouver dans le code. C'est un bug de gestion d'erreurs, comme un exception non rattrapée mais qui aurait du l'être.

Un programmeur C aurait pu faire de même :

if (ptr == NULL) { exit };
/* on peut déréférencer le ponteur dans la suite */

mais là où unwrap apporte tout de même une sécurité mémoire, c'est qu'il ne déréférencera jamais un pointeur NULL, là où un programmeur C peut oublier d'écrire le test. La fonction fold (règle d'élimination, règle d'usage) exige un traitement pour le cas des erreurs, traitement qui dans le cas de unwrap est un panic. Cette exigence n'existe ni en C, ni en C++. ;-)

Le cas des pointeurs est en fait équivalent au type Option, qui lui-même est équivalent au type Result où le type E des erreurs est un singleton.

Après, si tu regardes les règles sur l'absurde sur la page wikipdéia (ce qui se passe ici, il y a une erreur parce que l'entrée est contradictoire avec les conditions dont à besoin la fonction pour avoir un résultat), en réfléchissant un peu tu pourras te convaincre que les règles la concernant correspondent au fonctionnement des exceptions (en particulier le raisonnement par l'absurde qui décharge l'hypothèse, c'est lever un exception avec sa backtrace : la série de raisonnement qui ont mener à la contradiction).

Mais pour gérer les exceptions avec le type Result, il faut utiliser le ? en Rust. C'est la façon idiomatique d'utiliser ce que les programmeurs fonctionnels appellent le bind :

bind v f = fold f error v

Autrement dit on applique le traitement f en cas de succès et on fait remonter les erreurs à l'appelant, charge à lui de gérer l'erreur (si possible sans panic).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Bref faudrait lire des travaux de conservateurs, de gens de musée et d'historiens plus que LinuxFr.org j'imagine, pour répondre aux questions que je me pose sur l'instant.

Je demanderai ce week-end à une de mes soeurs qui travaillent comme responsable au service de conservation-restauration du musée des Arts et Métiers.

Mais à mon avis, vu le prix de la mise aux enchères, ils n'ont pas les moyens. Ils récupèrent beaucoup d'objets par dons de collectionneurs privés (comme le labo de Lavoisier), ou en achètent certains, mais là ce doit être trop chers pour eux. Et ensuite, il faut gérer, pour les problèmes de conservation, leurs administrateurs incompétents : faire des soirées mondaines avec champagne et musique à 120 dB (dégâts irréparables sur le pendule de Foucault qui ne supporte pas une telle pression acoustique), prêts à d'autres musées dans des conditions contraires aux préconisations des restaurateurs (une horloge qui revient cassée) et j'en passe…

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Par contre sa syntaxe est un peu hermétique de prime abord

En toute curiosité, que trouves-tu d'hermétique dans sa syntaxe ? Personnellement, je la trouve claire dans l'ensemble.

Le premier point qui m'interpelle est la syntaxe sur les types paramétriques où l'argument est placé devant la fonction, tout cela à cause d'une mauvaise influence de la grammaire anglaise : en anglais on écrira l is an int list, ce qui donne l : int list en OCaml (le : d'un jugement de typage étant le verbe être d'un jugement prédicatif, comme dans Socrate est mortel), là où je préférerais l : list int, le type paramétrique list étant une fonction des types dans les types que l'on applique ici à l'argument int. Cette syntaxe étant celle de tous les autres langages basés sur Curry-Howard, et qui est celle de l'application de fonction quand elle concerne les valeurs et non les types en OCaml.

Le second est la syntaxe des modules de première classe qui permettent de considérer les types classes de Haskell ou les traits de Rust comme des valeurs de première classe (ce qu'ils ne sont pas dans ces langages, étant gérés uniquement par le compilateur). Si j'ai un trait Showable (un type que l'on peut convertir en chaînes de caractères), on se retrouve avec des interfaces ayant cette signature

val foo : (module M : Showable with type t = 'a) -> 'a -> foo

ce qui est un peu lourd. Là où je préférerais une syntaxe plus légère de la forme

val foo : (module M : Showable) -> M.t -> foo

Le premier point risque de rester pour toujours pour des raisons historiques, le second est un PR en attente de validation qui, en plus de simplifier la syntaxe, enrichit grandement les possibilités d'usage des modules de première classe.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

En quoi la philosophie morale de Nietzsche, qui pourrait se résumer au principe « c'est un privilège que la nature a accordé au plus fort, que de se faire obéir des plus faibles », peut-elle être d'une quelconque utilité. Si je dois chercher des figures de l'ubermensch (le surhomme) nietzschéen des nos jours, je le vois plutôt chez Trump, Munsk ou Thiel. L'article du lien, en plus d'être une bouse générée par un LLM (si même l'ACM sy'met…), n'a rien à voir avec la philosophie de l'auteur de Par delà le bien et le mal, La généalogie de la morale ou encore Le crépuscule des Idoles.

Mais revenons à notre sujet : le problème de l’autre origine du concept bon, du concept bon tel que l’homme du ressentiment se l’est forgé, attend une solution concluante. Que les agneaux aient l’horreur des grands oiseaux de proie, voilà qui n’étonnera personne : mais ce n’est point une raison d’en vouloir aux grands oiseaux de proie de ce qu’ils ravissent les petits agneaux. Et si les agneaux se disent entre eux : « Ces oiseaux de proie sont méchants ; et celui qui est un oiseau de proie aussi peu que possible, voire même tout le contraire, un agneau — celui-là ne serait-il pas bon ? » — il n’y aura rien à objecter à cette façon d’ériger un idéal, si ce n’est que les oiseaux de proie lui répondront par un coup d’œil quelque peu moqueur et se diront peut-être : « Nous ne leur en voulons pas du tout, à ces bons agneaux, nous les aimons même : rien n’est plus savoureux que la chair tendre d’un agneau. » — Exiger de la force qu’elle ne se manifeste pas comme telle, qu’elle ne soit pas une volonté de terrasser et d’assujettir, une soif d’ennemis, de résistance et de triomphes, c’est tout aussi insensé que d’exiger de la faiblesse qu’elle manifeste de la force.

Nietzsche, Généalogie de la morale.

Le wokisme, voilà une morale du ressentiment bonne pour les agneaux ! Rien qui ne puisse plaire à Nietzsche, qui devrait se boucher le nez devant une telle puanteur. Rien de plus étranger à la noblesse aristocratique du surhomme, qui pose et affirme ses valeurs sans avoir besoin d'un dominant face auquel s'opposer : c'est une morale d'esclave !

S'il y a bien un philosophe qu'il faut combattre, c'est lui ! Toujours dans sa Généalogie de la morale :

Le latin malus (que je mets en regard de μέλας, noir) pourrait avoir désigné l’homme du commun d’après sa couleur foncée, et surtout d’après ses cheveux noirs (hic niger est), l’autochtone pré-aryen du sol italique se distinguant le plus clairement par sa couleur sombre de la race dominante, de la race des conquérants aryens aux cheveux blonds. Du moins le gaëlique m’a fourni une indication absolument similaire : — c’est le mot fin (par exemple dans Fin-Gal), le terme distinctif de la noblesse, en dernière analyse le bon, le noble, le pur, signifiait à l’origine : la tête blonde, en opposition à l’autochtone foncé aux cheveux noirs. Les Celtes, soit dit en passant, étaient une race absolument blonde ; quant à ces zones de populations aux cheveux essentiellement foncés que l’on remarque sur les cartes ethnographiques de l’Allemagne faites avec quelque soin, on a tort de les attribuer à une origine celtique et à un mélange de sang celte, comme fait encore Virchow : c’est plutôt la population pré-aryenne de l’Allemagne qui perce dans ces régions. (La même observation s’applique à presque toute l’Europe : en fait, la race soumise a fini par y reprendre la prépondérance, avec sa couleur, la forme raccourcie du crâne et peut-être même les instincts intellectuels et sociaux : — qui nous garantit que la démocratie moderne, l’anarchisme encore plus moderne et surtout cette tendance à la Commune, à la forme sociale la plus primitive, chère aujourd’hui à tous les socialistes d’Europe, ne soient pas, dans l’essence, un monstrueux effet d’atavisme — et que la race des conquérants et des maîtres, celle des aryens, ne soit pas en train de succomber même physiologiquement ?…)

Effectivement, ça fait envie ¿

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je ne pourrais dire mieux que la phrase concluant son article :

Ils ne sont qu’une arme de plus dans la guerre que le consumérisme mène contre l’intellectualisme.

Qui redit, à sa façon, ce que Goerges Bernanos disait dans La France contre les robots en 1946 :

On ne comprend absolument rien à la civilisation moderne si l'on n'admet pas d'abord qu'elle est une conspiration contre toute forme de vie intérieure.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Quand on écoute les collègues cosmologistes, ils vous disent qu'il n'est pas exclu que ~95% (estimation au doigt mouillée évidemment) de la nature de l'univers échappe actuellement à notre connaissance — les hypothétiques matières noires et énergies noires. Moi qui ait souvent du mal à résoudre un casse-tête que je puisse connaître entièrement, je conçois mal la niveau d'hubris qu'il faudrait avoir, pour prétendre décider du niveau de connaissance impliqué par le titre à partir de si peu (~5%).

J'ai recherché le texte de Kant sur les limites de la connaissance humaine. Je le cite pour la clarté avec laquelle il expose le problème :

La conscience de mon ignorance (si cette ignorance n’est en même temps reconnue comme nécessaire), au lieu de terminer toutes mes recherches, est au contraire la véritable cause qui les provoque. Toute ignorance porte ou bien sur les choses, ou bien sur la détermination et les bornes de ma connaissance. Or, quand l’ignorance est accidentelle, elle doit me pousser, dans le premier cas, à soumettre les choses (les objets) à une investigation dogmatique, et, dans le second, à rechercher, au point de vue critique, les limites de ma connaissance possible. Mais que mon ignorance soit absolument nécessaire, et que par conséquent elle me dispense de toute recherche ultérieure, c’est ce que l’on ne peut prouver empiriquement par l’observation, mais seulement d’une manière critique, en sondant les sources premières de notre connaissance. La détermination des limites de notre raison ne peut donc se faire que suivant des principes à priori, mais nous pouvons connaître aussi à posteriori qu’elle est bornée, en remarquant ce qui, dans toute science, nous reste encore à savoir, bien que cette connaissance d’une ignorance à jamais invincible soit encore indéterminée pour nous. La première connaissance de l’ignorance de la raison, que peut seule nous donner la critique de la raison même, est donc une science ; mais la seconde connaissance n’est qu’une perception, aux suites de laquelle je ne puis assigner des limites. Quand je me représente (suivant l’apparence sensible) la surface de la terre comme un plateau rond, je ne puis savoir jusqu’où elle s’étend. Mais l’expérience m’apprend que, où que j’aille, je vois toujours devant moi un espace où je puis continuer de m’avancer, et je reconnais ainsi les bornes de ma connaissance réelle de la terre, mais non pas celles de toute description possible de la terre. Que si j’en suis venu au point de savoir que la terre est un globe et que sa surface est sphérique, je puis alors connaître d’une manière déterminée et suivant des principes à priori, même par une petite partie de cette surface, un degré par exemple, le diamètre de la terre, et, par ce diamètre, la complète circonscription de la terre, c’est-à-dire sa surface entière ; et, bien que je sois ignorant par rapport aux objets que cette surface peut contenir, je ne le suis pas quant à la circonscription qui les contient, à son étendue et à ses limites.

Kant, Critique de la Raison Pure.

Comme c'est un problématique de ce genre que traite les auteurs :

Mais que mon ignorance soit absolument nécessaire, et que par conséquent elle me dispense de toute recherche ultérieure, c’est ce que l’on ne peut prouver empiriquement par l’observation, mais seulement d’une manière critique, en sondant les sources premières de notre connaissance.

afin de répondre par la négative au sixième problème de Hilbert, il n'ont pas grand choix sur la méthode. Je ne connais que trois résultats utilisables en la matière :

• l'incomplétude de Gödel (limites de la déduction)
• le problème de l'arrêt de Turing (limites du calcul)
• la critique kantienne (limites de la raison théorique dans son usage philosophique)

Vu la question (existence d'un système axiomatique), il n'ont pas d'autres choix que de passer par l'incomplétude de Gödel. Il l'utilise correctement en l'appliquant à un système adéquate aux hypothèses du théorème (contrairement à Régis Debray. Mais une fois obtenue l'incomplétude déductive du système, le reste de l'argumentaire devient de plus en plus douteux.

D'ailleurs, les mathématiciens (toujours dans le cadre du programme de Hilbert) ont eux aussi cherché un système axiomatique unique dans lequel toutes les mathématiques connues pourraient se formaliser (un anneau pour les gouverner tous ;-). Rien ne disait que c'était faisable, et ce fût fait sous la forme de la théorie axiomatique des ensembles ZF. Elles est bien entendue incomplète, car soumise au théorème d'incomplétude, mais cela n'a jamais perturbé personne. On n'a nullement invoqué je ne sais quel entendement non algorithmique en conséquence. Bien au contraire, cela a ouvert un champ de recherche luxuriant : quels sont les énoncés ayant un sens mathématique important qui sont indécidables dans ZF ? On a au choix : toutes les formes de l'axiome du choix, l'hypothèse du continue de Cantor, l'existence ou non de partie des réels non mesurables au sens de Lebesgue, les axiomes sur les grands ordinaux… Cela a donné des résultats, dits de consistance relative, analogues à ceux obtenus par Poincaré sur la consistance relative des différentes géométries (euclidienne, hyperbolique et sphérique). Et toutes ces mathématiques sont algorithmiques de part en part, du moins on a pour l'instant ZF + Choix dépendant en logique classique interprété comme programmes via Curry-Howard, et ce système est suffisant pour développer tout l'outillage conceptuel actuellement utilisé par les physiciens théoriciens.

Et malgré cela, certains continuent, à bon droit, de chercher des théories concurrentes à ZF, à commencer par la théorie homotopique des types (HoTT) ou celle spéculative du sujet de thèse de Jeanas.

Après, que l'entendement humain soit non algorithmique, je n'en doute pas une seconde. Mais c'est parce qu'il ne sert pas qu'à faire des mathématiques, il sert aussi à philosopher. L'usage mathématique est algorithmique, pas son usage philosophique. Ça c'est Kant qui l'a prouvé.

Les mathématiques donnent le plus éclatant exemple d’une heureuse extension de la raison pure par elle-même et sans le secours de l’expérience. Les exemples sont contagieux, surtout pour cette faculté, qui se flatte naturellement d’avoir toujours le même bonheur qu’elle a eu dans un cas particulier. Aussi la raison pure espère-t-elle pouvoir s’étendre, dans son usage transcendental, avec autant de bonheur et de solidité qu’elle l’a fait dans son usage mathématique, surtout en appliquant ici cette même méthode qui lui a été là d’une si évidente utilité. Il nous importe donc beaucoup de savoir si la méthode qui conduit à la certitude apodictique, et que dans cette dernière science on appelle mathématique, est identique à celle qui sert à chercher cette même certitude dans la philosophie et qui y devrait être appelée dogmatique.

La connaissance philosophique est la connaissance rationnelle par concepts, et la connaissance mathématique la connaissance rationnelle par construction des concepts. Construire un concept, c’est représenter à priori l’intuition qui lui correspond. La construction d’un concept exige donc une intuition non empirique, qui par conséquent, comme intuition, soit un objet singulier, mais qui n’en exprime pas moins, comme construction d’un concept (d’une représentation générale), quelque chose d’universel qui s’applique à toutes les intuitions possibles appartenant au même concept. Ainsi je construis un triangle en représentant l’objet correspondant à ce concept soit par la simple imagination dans l’intuition pure, soit même, d’après celle-ci, sur le papier dans l’intuition empirique, mais dans les deux cas tout à fait à priori, sans en avoir tiré le modèle de quelque expérience. La figure particulière ici décrite est empirique, et pourtant elle sert à exprimer le concept sans nuire à son universalité, parce que, dans cette intuition empirique, on ne songe jamais qu’à l’acte de la construction du concept, auquel beaucoup de déterminations sont tout à fait indifférentes, comme celles de la grandeur, des côtés et des angles, et que l’on fait abstraction de ces différences qui ne changent pas le concept du triangle.

La connaissance philosophique considère le particulier uniquement dans le général, et la connaissance mathématique le général dans le particulier, même dans le singulier, mais à priori et au moyen de la raison, de telle sorte que, comme ce singulier est déterminé d’après certaines conditions générales de la construction, de même l’objet du concept auquel ce singulier ne correspond que comme son schème doit être conçu comme universellement déterminé. […]

Puisque nous nous sommes fait un devoir de déterminer exactement et avec certitude les limites de la raison pure dans l’usage transcendental, mais que cette faculté a ceci de particulier que, malgré les avertissements les plus pressants et les plus clairs, elle se laisse leurrer par l’espoir de parvenir, par de là les limites des expériences, dans les attrayantes contrées de l’intellectuel, il est nécessaire de lui enlever encore en quelque sorte la dernière ancre d’une espérance fantastique, en lui montrant que l’application de la méthode mathématique dans cette espèce de connaissance ne peut lui procurer le moindre avantage, si ce n’est peut-être celui de lui découvrir plus clairement ses propres défauts ; que la géométrie et la philosophie sont deux choses tout à fait différentes, bien qu’elles se donnent la main dans la science de la nature, et que par conséquent les procédés de l’une ne peuvent jamais être imités par l’autre.

La solidité des mathématiques repose sur des définitions, des axiomes et des démonstrations. Je me contenterai de montrer qu’aucun de ces éléments ne peut être ni fourni ni imité par la philosophie dans le sens où le mathématicien le prend ; que le géomètre, en transportant sa méthode, dans la philosophie, ne construit que des châteaux de cartes ; que le philosophe, en appliquant la sienne aux mathématiques, ne peut faire que du verbiage ; ce qui n’empêche pas que le rôle de la philosophie dans cette science ne soit d’en reconnaître les limites, et que le mathématicien lui-même, quand son talent n’est pas déjà circonscrit par la nature et restreint à sa sphère, ne soit obligé de tenir compte des avertissements de la philosophie et de ne pas se mettre au-dessus d’eux.

Kant, Critique de la Raison Pure

Et la physique a tout autant besoin de la philosophie que des mathématiques pour justifier ses premiers principes, à commencer par le principe de causalité, et pour se faire elle ne peut emprunter la méthode algorithmique des mathématiques.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Si je comprends bien, il ne s'agit pas ici de créer un "univers" (un système formel) sans contrainte a priori par rapport à la réalité physique mais de reformuler (donc a posteriori) sous forme d'axiomes les postulats d'une théorie physique sur le réel pour s'assurer de leur "validité", "objectivité", consistance, …

Oui, on ne va tout de même pas prétendre pouvoir faire sortir, comme par magie, de notre esprit, des lois de la nature qui ne peuvent être connus que par expérience.

Comme je l'ai dit par analogie avec la programmation, les spécifications, bien que formalisées et constituant une axiomatique du domaine métier, ne peuvent être formulées que par la connaissance expérimentale du dit domaine. Et l'on y retrouve les deux classes de bugs dans les logiciels : non conformité du code avec les spécifications (c'est là que les systèmes de types jouent un rôle), non conformité des spécifications avec le domaine (cela, aucune méthode formelle ne peut les résoudre).

Cela étant, il reste toujours un part d'a priori dans les théories physiques, que l'on ne peut totalement éliminer pour tout ramener à l'expérience. C'est cela que Kant avait formidablement remarqué (on le retrouve dans Curry-Howard) et que Hilbert espérait résoudre via l'axiomatisation de la physique. On le retrouve dans ce passage de l'article :

Autrement dit, l'axiomatisation de la physique nous permet de nous dégager de la géométrie euclidienne, qui, provenant de notre intuition spatiale, était jusqu'à présent un présupposé
anthropomorphique implicite à notre conception de la structure du monde empirique. Or, en axiomatisant la physique, il devient possible de se dégager de ce présupposé et ainsi atteindre une connaissance plus objective.

Pour un kantien, il restera toujours un fond a priori dans les sciences de la nature. Voir par exemple l'exemple des lois de l'electricité par Ampère, décrite dans cette article : La déraisonnable efficacité des mathématiques. Comme dit dans l'article, c'est lié à ce que Kant appelait sa théorie du schématisme, ce qu'exprime à sa façon la correspondance preuve-programme : les preuves sont des programmes, c'est-à-dire des schèmes (en terme kantien), et l'on ne peut s'en passer pour appréhender le réel. J'aime beaucoup les deux citations de Paul Valéry qui sont si kantienne dans l'esprit :

La mathématique est la science des actes sans les choses et par là des choses que l'on peut définir par des actes.

Quand les contenus sont créés par les opérations mêmes, c'est-à-dire quand quand des opérations remarquées sont désignées, isolées et qu'on en forme des combinaisons, alors on est en mathématiques

Paul Valéry.

On le retrouve dans la conférence donnée par Stéphane Mallat lors du colloque de rentrée au Collège de France sur l'intelligence artificielle : Mystères mathématiques d’intelligences pas si artificielles. À partir de la quatrième minute, il aborde la théorie de la connaissance et les deux tendances qui s'opposent depuis l'antiquité : rationalisme contre empirisme (Platon contre Aristote). Il évoque plus particulièrement David Hume (empiriste) qui mit en doute la notion même de causalité, et Kant qui vint développer la troisième voie : la méthode critique entre le dogmatisme rationaliste et le scepticisme empirique. Il soutient que l'approche des réseaux neurones tient du kantisme mais ne développe pas trop ses raisons, si ce n'est qu'il y a, aussi, une dimension d'a priori dans les réseaux de neurones.

Mais je veux surtout rebondir sur Hume, la causalité et son rapport à Kant. C'est Hume qui fit sortir Kant de son sommeil dogmatique (l'expression est de Kant lui-même) par son attaque contre le principe de causalité. Et la réponse de Kant fut ce qu'il est convenu d'appeler sa théorie des catégories qui est une correspondance preuve-programme bien avant l'heure : la Critique de la Raison Pure date de 1781 et la dite correspondance de la fin des années 1960. La réponse de Kant à Hume fut celle-ci : le principe de causalité n'est pas d'origine empirique, mais nous l'imposons a priori au réel en conformité avec la forme logique des jugements hypothétiques.

Que voulait-il dire par là ? Faisons un détour par la théorie de la démonstration. Parmi les règles de déduction employées par les mathématiciens, il y en a une bien connue sous le nom de modus ponens : si A alors B, or A donc B. Et cette règle est celle qui sert à typer l'application de fonction dans les langages fonctionnels (c'est la base de la correspondance de Curry-Howard). Mais cette règle de typage a un principe analogue dans l'analyse formelle des langages impératifs, c'est le cœur de logique de Hoare avec ses triplets de Hoare {P} C {Q} : un programme C a pour résultat de passer de P à Q. Autrement si ma machine est dans l'état P alors en éxécutant le programme C, elle sera dans l'état Q. Et c'est explicitement ce que Kant avait exposé dans sa table des catégories, via la correspondance entre la table des jugement et la table des catégories. Où l'on voit la correspondance entre les jugements hyptothétiques (si A alors B) et la causalité. Correspondance qu'exprime à leur manière Curry-Howard et Hoare : les programmeurs fonctionnels composent les fonctions, comme les programmeurs impératifs composent les instructions. Et c'est ce lien entre ces deux logiques qui expliquent pourquoi l'on peut automatiser (c'est à dire construire des machines soumises à la causalité) l'exécution des algorithmes et non les exécuter seulement à la main.

On retrouve cette correspondance de la logique dans la confrontation même des théories physiques avec l'expérience. La physique pose une loi causale (en arrière plan, il y a la forme logique si A alors B), constate un état A et observe non B : il y a contradiction entre le réel et la théorie. Conséquence : soit la loi est fausse, soit l'état A était mal déterminé. Deux exemples issu de de la cosmologie :

• les perturbations orbitales de Mercure ne correpondent pas aux observations : on prédit B mais on observe non B, on émet l'hypothèse de l'existence d'une autre planète (on pose non A), à savoir Pluton, sans changer la loi ;
• le périhélie de Mercure ou la déviation des rayons lumineux par le Soleil, on change la loi (le si A alors B) et on passe à la relativité générale.

Là tu te dis peut être : mais what the fuck !? De quel droit peut-on imposer totalement a priori des lois à la nature (non selon le contenu mais selon la forme) sans même les emprunter à l'expérience ? C'est là que Kant et les kantiens répondent en cœur avec l'enfant bouddhiste de Matrix : la cuillière n'existe pas ! :-P Derrière cette boutade, il y a le principe que si l'on voit partout de l'espace et du temps dans l'expérience, c'est parce qu'on les y met nous mêmes. Donc, d'un point de vue expérimentale, la cuillère existe bien, certes, comme objet spatio-temporellement déterminable. Mais si l'on fait abstraction de son rapport à un observateur, et que l'on se demande : cette chose qui nous apparaît sous la forme d'une cuillière, est-elle en elle même dans l'espace et dans le temps, soumise à la causalité… À cela nous répondons : non ! En tant qu'objet d'expérience possible elle l'est, mais abstraction faite du rapport à l'expérience elle ne l'est pas. Il n'y a pas de réalité absolument indépendante de l'esprit humain qui serait objet d'étude de cette science que l'on nomme physique.

Par exemple, reformuler les six postulats de la mécanique quantique sous forme d'axiomes, ça a été tenté ?

Je ne sais pas. Je ne suis pas assez les travaux de physiciens théoriciens pour le savoir, mais il y a de très forte chance qu'il y ait eu des tentatives.

Pour en revenir à l'objet du lien, utiliser le concept d'axiomatisation de la physique malgré sa nature très différente de l'axiomatisation des systèmes formels pour y faire des "démonstrations" basées sur ce qui a été démontré dans le cadre d'un système formel (les théorèmes de Gödel, notamment) me paraît douteux mais je n'ai largement pas le niveau pour aller au delà de ce doute "naïf". Je note cependant que tu n'es pas davantage convaincu.

Leur usage du théorème d'incomplétude est parfaitement valide. Ce que je ne comprends pas c'est quand ils arguent l'existence de phénomènes observables, donc dont on peut déterminer la valeur de vérité, qui sont hors du champ de la déductibilité du système : il y a des formules non déductibles, le système étant déductivement incomplet, mais en quoi correspondent-elles à des phénomènes observables ? De mémoire, chez Penrose, c'est le phénomène de réduction de la fonction d'ondes ou réductions du vecteur d'états en mécanique quantique qui l'amène à développer sa notion d'entendement non algorithmique. Mais dans cet article, bien court et peu développé, les principes tombent un peu comme un cheveux sur la soupe. Donc je ne sais quoi en dire, d'autant que je suis loin d'être un spécialiste du sujet. Mais je doute qu'il puisse convaincre ceux qui s'occupent du sixième problème de Hilbert.

Pour finir, avec une remarque quelque peu hors-sujet. Kant ne s'est pas contenté de faire usage de son système pour justifier l'usage des mathématiques en physique et la légitimité de certains principes a priori. Il l'a même étendu à la doctrine du droit et à la philosophie politique. Question : pourquoi nos États sont-ils structurés autour de trois pouvoirs (législatif, exécutif et judiciaire). Réponse :

Tout État renferme en soi trois pouvoirs, c’est-à-dire que l’unité de la volonté générale s’y décompose en trois personnes (trias politica) : le souverain pouvoir (la souveraineté), qui réside dans la personne du législateur ; le pouvoir exécutif, dans la personne qui gouverne (conformément à la loi) ; et le pouvoir judiciaire (qui attribue à chacun le sien suivant la loi), dans la personne du juge (potestas legislatoria, rectoria et judiciaria). Ce sont comme les trois propositions d’un syllogisme pratique : la majeure, qui contient la loi d’une volonté ; la mineure, l’ordre de se conduire d’après la loi, c’est-à-dire le principe de la subsomption des actions sous cette loi ; enfin la conclusion (la sentence), qui décide ce qui est de droit dans le cas dont il s’agit.

Kant, Doctrine du droit.

Autrement dit : nous ne faisons que projeter dans la constitution de nos États la structure formelle de notre propre esprit : raison (législatif), entendement (exécutif) et faculté de juger (législatif).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Alors je vais sûrement passer pour l'ignare de service qui s’immisce dans un débat qui le dépasse mais j'assume : c'est comme ça qu'on apprend :-)

Si je peux te donner conseil : conserve précieusement cette maxime, et ne cesse jamais d'en faire usage.

Le même prof qui avait plaisanté sur les sanctifiés du Pape nous avait donné ce principe dès les premières minutes de son premier cours :

Si vous ne comprenez pas quelque chose, n'hésitez pas à m'interrompre. Je m'arrêterais pour expliquer. Autrement, je continuerais partant du principe que vous avez compris.

Je n'ai jamais hésité à l'interrompre, et il a toujours satisfait à ma requête. Néanmoins, dans le cadre d'une salle de classe, j'ai pu constaté que nombreux sont ceux n'ayant jamais osé (bien qu'il ne comprenait pas), sans doute de peur de passer pour des idiots. Le problème de la peur du regard des autres…

Du coup, ça veut dire quoi, une axiomatisation de la physique ?

Il faut voir cela avec David Hilbert, c'est son sixième problème.

Le sujet étant long et complexe, j'ai trouvé ce texte en ligne : la portée epistémique de l'axiomatisation de la physique chez Hilbert. Cela reste tout de même un texte très technique qui revient tout d'abord sur l'utilité et la raison d'être de l'axiomatisation pour les mathématiques, avant de traiter de la volonté d'Hilbert d'étendre la méthode à la physique.

Mais sinon, en version plus simple et courte : c'est ce que font tous les programmeurs du monde. Lorsqu'une équipe de programmeurs établit un cahier des charges puis écrit les spécifications du logiciel qu'ils doivent écrire, ils axiomatisent leur domaine métier. Ensuite charge à eux de réifier cette axiomatique, c'est à dire implémenter les spécifications.

C'est là qu'intervient l'utilité pour les programmeurs du domaine de recherche de Jeanas, la théorie des types et la correspondance preuve-programme. Un système de type est un langage dans lequel on peut exprimer ses spécifications, le type checker vérifiant que le code est conforme aux types. Plus le systèmes de types est évolué, plus on peut exprimer finement ses spécifications, et moins il y a de bug (de code non conforme aux spécifications). Et c'est ce qu'on toujours fait les mathématiciens : la preuve d'un théorème est un programme dont l'énoncé est la spécification. Prenons l'exemple du théorème affirmant qu'il existe un nombre infini de nombres premiers. Celui-ci affirme que « pour tout entier n, il existe un entier p premier et strictement plus grand que n ». Toute preuve de ce théorème est un programme qui prend en entrée un entier n, et renvoie en sortie un entier p premier et plus grand que l'entrée. C'est cela la correspondance de Curry-Howard ou correspondance preuve-programme (toute preuve mathématique a un contenu algorithmique, est un programme). Vérifier qu'une preuve est logiquement valide (elle respecte bien les règles de déduction et les axiomes de la théories) ou vérifier qu'un programme est bien typé, c'est tout un ! Un vérificateur de preuves ou un type checker, c'est le même logiciel.

Sur le sujet, il y a ce texte bien plus abordable à lire et comprendre que le premier (je te le conseille pour commencer): À propos de la théorie des démonstrations (du programme de Hilbert aux programmes tout court). L'auteur est aussi un de mes anciens professeurs, celui qui m'initia à ce domaine de la logique. Il est l'auteur d'une machine abstraite La machine de Krivine dont le but était d'interpréter les preuves de théorèmes comme des programmes. Elle est proche, dans son fonctionnement, à la première machine abstraite qui interprétait le bytecode du langage OCaml (la ZINC).

Sinon, pour revenir à de la programmation de tous les jours : utiliser un types primitif d'un langage, c'est poser une axiomatique (tout ce que le langage fournit sur ce type est une axiomatique); programmer contre une classe abstraite, c'est poser une axiomatique (celle décrite par l'interface de la classe); utiliser des interfaces en golang, c'est faire de l'axiomatique (celle décrite par l'interface); utiliser des traits en Rust idem, des types classes en Haskell idem, des foncteurs en OCaml idem… Je n'ai jamais croisé un développeur de ma vie qui ne faisait pas de l'axiomatique sans le savoir (à la manière de monsieur Jourdain).

Enfin, c'est pour cela que je suis sur un site dédié aux logiciels libres : de même qu'une preuve mathématique se doit d'être publique, un code doit l'être; conceptuellement ce ne sont pas deux types d'objets distincts, mais les deux faces d'une seule et même pièce.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Donc c'est plus en lien avec la théorie de la démonstration et la correspondance de Curry-Howard ou correspondance preuves-programmes. Tu es plus du côté informatique (systèmes de types pour les langages de programmation) ou mathématique (HoTT, interprétation des preuves comme programmes, logique classique ou intuitionniste) ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Juste deux petits exemples pour contextualiser ce jugement à l'emporte pièce sur la seule base du titre

Ce jugement semble ne pas avoir été apprécié par un membre du site, à en juger par ma note.

Dans les années 90, les meilleurs physiciens appliqués, spécialisés en traitement du signal, armés de solides théorèmes mathématiques nous démontraient irréfragablement les limites théoriques en matière de signal transporté sur du câble en cuivre (les fameux xx kbauds). Puis quelqu'un inventa l'ADSL…

À la même époque, d'autres physiciens (Sokal et Bricmont) reprochaient à certains philosophes français leur usage saugrenu de l'incomplétude de Gödel.

Quand on écoute les collègues cosmologistes, ils vous disent qu'il n'est pas exclu que ~95% (estimation au doigt mouillée évidemment) de la nature de l'univers échappe actuellement à notre connaissance — les hypothétiques matières noires et énergies noires. Moi qui ait souvent du mal à résoudre un casse-tête que je puisse connaître entièrement, je conçois mal la niveau d'hubris qu'il faudrait avoir, pour prétendre décider du niveau de connaissance impliqué par le titre à partir de si peu (~5%).

L'un n'empêche pas l'autre. Notre connaissance peut être bornée quant aux contenu du monde (bornée par ce qu'il reste encore à découvrir) mais nous pouvons être en mesure de déterminer les limites du savoir humain (ce que font les méthodes formelles). Kant avait une belle image pour illustrer cela : je peux ignorer le contenu effectif de la surface du globe (il faudrait pour cela en avoir parcouru la totalité) tout en sachant qu'il est circonscrit dans des limites données que je peux déterminer (je n'ai pas besoin de le parcours pour connaître sa circonférence).

Cela étant j'ai fini par lire l'article est je suis moins catégorique que Jeanas sur son contenu : ce n'est pas du Régis Debray. La thèse principale n'est pas tant que nous ne vivons pas dans une simulation, mais qu'une théorie du tout qui unifierait la relativité générale et la physique quantique n'est pas axiomatisable. En résumé : la physique n'est pas axiomatisable. Ce qui a pour corrolaire que l'univers n'est pas une simulation d'ordinateur.

Dans l'ensemble, bien que je souscrives personnellement à ces thèses métaphysiques, leur argumentaire ne me convainc que moyennement. D'une part parce que je doute que la méthode mathématique soit la seule à même de traiter ces questions. D'autre part, parce que l'article consiste à formaliser la thèse de Roger Penrose d'entendement non algorithmique (non algorithmic understanding), thèse qu'il développe par exemple dans son livre Les deux infinis et l'esprit humain. Cette thèse me semblait pas très claire à l'issue de ma lecture du livre, et l'article ne change pas la donne dessus.

Ils font effectivement usage des deux théorèmes de Gödel que j'ai évoqué dans mon premier commentaire. Tout commence à la troisième page de l'article, lorsqu'il suppose une axiomatisation de la physique en supposant l'existence d'un système formel , dont la signification doit vouloir dire : Formalisation of Quantic Gravitation. Il font sur le système des hypothèses raisonnables : logique du premier ordre, ensemble d'axiomes récursivement énumérables, système complet de règles d'inférence. À dire vrai, ces derniers hypothèses n'en sont pas, c'est la définition même de la proposition « la physique est axiomatisable ».

À cela ils ajoutent deux contraintes :

• l'arithmétique de Peano est dérivable dans ce système axiomatique ;
• tout les phénomènes observables sont prévisibles par la théorie (conséquence du système d'axiomes par les règles de déduction)

On peut bien leur accorder la première, la physique théorique ayant besoin de l'arithmétique. C'est celle-ci qui leur permet de faire usage du théorème d'incomplétude : le système axiomatique étant une extension de l'arithmétique de Péano, il est déductivement incomplet.

Mais ensuite, je dois avouer avoir du mal à les suivre dans leur pensée. Ils semblent jongler entre syntaxe et sémantique : il y aurait des énoncés observables, et donc vrais (théorie de la vérité correspondance, sémantique de Tarski), dans l'univers (cf. deuxième contrainte), mais qui ne seraient pas conséquences déductives du système d'axiomes (que l'on pourrait obtenir à partir des axiomes de l'ensemble Sigma et des règles R). Peut être bien, mais lesquelles ? C'est à partir de là qu'ils introduisent leur méta-théorie non algorithmique, leur entendement non algorithmique à la Penrose et qu'ils me perdent. Non que ce genre de méta-théorie ne soient pas considérées par les logiciens mathématiciens (en théorie des modèles, on étudie bien les modèles non standard de l'arithmétique, des théories non récursivement énumérables voir même non dénombrables), mais je ne comprends pas selon quels principes ils l'introduisent ni la justifient.

Ça a au moins l'intérêt de montrer certaines limites des systèmes de publications.

Cela me rappelle une blague de notre professeur de théorie des modèles, lorsque j'étais étudiant en DEA de logique mathématique et fondements de l'informatique. Il faut faire attention, ici, que le mot modèle est un homonyme de celui utilisé en physique (bien qu'il y ait des rapports entre les deux). Pour un théoricien des modèles, à la question qu'est-ce qu'un groupe ? Il répond : un modèle de la théorie des groupes, c'est à dire une structure qui satisfait à l'axiomatique de la théorie.

Trève de digression et revenons à sa blague. Un jour, en début du cours, il nous tint à peu près ce discours : « je lisais ce matin dans le Monde que la pape Jean Paul II avait sanctifié plus de personnes que tous ces prédécesseurs réunis. Sachant que, durant ces 20 dernières années, on a publié plus d'écrits mathématiques que durant toute la période de l'humanité qui précède, si un jour vous publiez un article insignifiant, vous pourrez vous considérer en bijection avec un sanctifié du pape ! ».

Je dois admettre, après lecture de l'article, que je ne sais quoi dire sur le statut de sanctifiés de ses auteurs.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Quand je vois ce genre de titre, je n'ai même pas envie de lire l'article. Ce n'est pas la première fois, ni la dernière, que l'on fera dire n'importe quoi aux théorèmes de Gödel. Mais même si les physiciens s'y mettent, on n'est pas sorti de l'auberge.

De toute façon, comme je suis kantien, la question n'a même pas de sens pour moi : comme dit le petit enfant boudhiste dans le premier Matrix, « la cuillère n'existe pas ». :-P

Tu fais une thèse en théorie de la démonstration ? ou en calculabilité ? C'est là où j'y vois trois résultats fondamentaux :

• théorème de complétude de Gödel
• théorème d'incomplétude de Gödel
• correspondance de Curry-Howard (logique intuitionniste et classique)

Théorèmes qui ne font que confirmer le cœur de la philosophie kantienne, et l'inexistence de la cuillère.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

il ne faut pas forcément prendre les chiffres pour argent comptant

Au delà de prendre les chiffres pour argent comptant, je vois ce que cela donne chez moi. En mai, pendant que je préparais ma terre, mon voisin se plaigner du manque d'eau, alors que, hormis le premier centimètre, mon sol état noir et gorgé d'eau.

Cherche un peu sur la chaîne agriculture vivrière et tu pourras constater la différence de structure entre deux terres à peine séparées de quelques dizaines de mètres (ce n'est pas chez moi, mais l'idée est la même). ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Le GIEC a tout un chapitre là dessus

Oui, je le sais. Hervé Coves traite des solutions du dernier rapport du GIEC dans un série de vidéo sur le thème « Le carbone, c'est la vie ».

Ton article parle d'expérimentations, c'est très bien mais il ne faut pas forcément prendre les chiffres pour argent comptant,

Sur cette article c'est une petite expérimentation (petite ferme en maraichâge). Mais il y a eu des expérimentations à plus grandes échelle en Suisse (canton de Vaud), où ils dépassent de loin l'objectif du 4 pour mille. Et dans la série de vidéos donnée au dessus (journée de conférence), il y a une usine de production de pop corn qui avance un bilan carbone bénéfique (elle séquestre plus de carbone qu'elle n'en émet), avec encore de la marge de manœuvre : 80% des terres sont en non labour (il reste 20% de marge de manœeuvre) et ils travaillent à la réduction sur le transport.

ça nécessite une vision à grande échelle quand même

Ça nécessite un changement de pratique, qui ne sera certainement pas facile à mettre en place : cela nécessite une remise en cause de 10_000 ans de pratiques agricoles. Il est sûr que cela ne se fera pas du jour au lendemain.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

C'est sans doute pas le cas et pour vraiment à revenir à l'état antérieur faudrait retirer énormément de CO2 de l'athmosphère et ça c'est encore en partie dépendant de paris technologiques (qui peuvent être source d'inaction).

Où alors, un des leviers d'actions est le recul d'usage de la technologie. Si nos agriculteurs rengeaient leurs tracteurs pour arrêter le labour, ils pourraient stocker dans le sol nos émissions annuelles, voir plus. Adopter les méthodes de sol vivant pour inverser son bilan carbone.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Il y va fort, Mr Phi, notamment quand il émet des doutes sur les aptitudes mathématiques de Luc Julia.

Je n'ai pas regardé la vidéo, donc je ne préjugerais pas des aptitudes de Luc Julia. En revanche mon expérience passée sur Mr Phi m'a amené cette conclusion : je ne doute pas de ses aptitudes en mathématiques, il n'en a aucune, et pour la philosophie, il est comme nombre des personnes formées à l'école française : s'il a une tête bien pleine (histoire de la philosophie), il n'est pas certain qu'elle soit bien faite. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Disons que je ne comprends pas sa sociologie de la science, peut-être d'ailleurs parce que ça correspond à une époque lointaine et que le fonctionnement de la science a beaucoup changé depuis.

Oui ça doit être cela, tu ne comprends pas sa sociologie des sciences. Je ne crois pas que celà ait beaucoup évolué depuis son époque, si ce n'est la hausse de volume de cette catégorie :

Mais beaucoup d'autres se rencontrent également en se Temple qui, exclusivement pour une raison utilitaire, n'offrent en contrepartie que leur substance cérébrale !

Et d'ailleurs, dans ton commentaire, tu décris très bien ce que cette catégorie apporte au bon fonctionnement du système.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Qu'est-ce qui t'ennuis dans ce texte (tronqué, la suite et bien plus inintéressante) ? Le fait que, malgré ton doctorat et ta carrière de chercheur, certaines personnes te considèrent comme une être secondaire ? tu as une revanches à prendre sur la vie ?

La vision d'Einstein est quand même celle d'un élitisme scientifique assez vertigineux

Elle est celle de ceux qui, comme pierre essentielle, font la Science. (Je n'en fait pas, moi même partie, mais mon intellect a besoin de ces personnes hors normes pour se nourrir).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Repousser un peu les limites ou améliorer la physique ou les maths ne signifie pas que ce soit le cas. Einstein a pu faire ça tout en restant humain (enfin, je crois ?).

Demandons donc son avis à Einstein sur la question du savoir et de la science.

Le temple de la Science se présente comme une construction à mille formes. Les hommes qui le fréquentent ainsi que le motivations morales qui y conduisent se révèlent tous différents. L'un s'adonne à le Science dans le sentiment de bonheur que lui procure cette puissance intellectuelle supérieure. Pour lui la Science se découvre le sport adéquat, la vie débordante d'énergie, la réalisation de toutes les ambitions. Ainsi doit-elle se manifester ! Mais beaucoup d'autres se rencontrent également en se Temple qui, exclusivement pour une raison utilitaire, n'offrent en contrepartie que leur substance cérébrale ! Si un ange de Dieu apparaissait et chassait du Temple tous les hommes qui font partie de ces deux catégories, ce Temple se viderait de façon significative mais on y trouverait encore tout de même des hommes du passé et du présent. Parmi ceux-là nous trouverions notre Planck. C'est pur cela que nous l'aimons.

Je sais bien que, par notre apparition, nous avons chasser d'un cœur léger beaucoup d'hommes de valeurs qui ont édifié le Temple de la Science pour une grande, peut être pour la plus grande partie. Pour notre ange, la décision serait bien difficile dans grand nombre de cas. Mais une constatation s'impose à moi. Il n'y aurait eu que des individus comme ceux qui ont été exclus, eh bien le Temple de ne se serait pas édifié, tout autant qu'une forêt ne peut pas s'édifier si elle n'est constituée que de plantes grimpantes !

Einstein, Comment je vois le monde.

Mon avis sur la question, qui marche dans les pas d'Einstein, est celui-ci : l'ange de Dieu se retrouve, de nos jours, avec un critère infaillible : ceux qui sont remplaçables par un automate n'aurait jamais pu édifier et ne contribuerons que marginalement à l'édification du temple de la Science. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je n'ai pas insisté sur mon message précédent. Mais crois tu vraiment aux coccinelles comme solutions miracles contre les pucerons ? Et produis-tu ta nourritures ou contes tu sur autrui pour le faire à ta place ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ya pas besoin d'avoir un doctorat en biochimie pour comprendre le consensus scientifique, lire le modus operandi et les conclusions d'études, et se faire une opinion.

Certes un doctorat biochimie n'est pas nécessaire, mais déjà se nourrir soi même devrais pauser des questions (et si on le pratique, le coup des coccinelles fait rire jaune).

Personnellement; je produis plus de 50% de ma nourriture végétale (sans pesticides, en mode maréchal sur sol vivant ;-) Et, honnêtement, bien que je souhaites les changements de pratiques, je ne suis pas sûr que cela puisses se faire du coq à l'âne.

Si notre espoir est celui-là : 

le chemin est celui là :

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Car peut être que « la vérité » n'existe pas (en tout cas celles de Isaac, d'Albert ou de Donald sont peut être différentes).

Soutiens-tu que la notion de vérité est vide de sens et qu'en conséquence il ne peut exister de science (quelque soit son objet d'étude) ?

si le savoir ne vient pas de l'expérience, d'où provient il ?

Là tu accordes qu'il existe un savoir, et donc une véritié des propositions qu'il contient. Mais alors penses-tu que les critères de vérités des mathématiques sont fondées sur l'expéreince ? Si c'est le cas, sache qu'aucun mathématicien au monde ne te l'accordera. ;-)

Alors, il reste la question d'où vient ce savoir : il est codé en dure dans notre faculté de savoir, l'expérience est l'occasion pour nous de le mettre en action et c'est lors de cette mise à l'épreuve que nous en prenons conscience.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Après réflexion, j'appelle cela une non réponse. Ma question était pourtant simple : comment une science qui ne prend pas ses critères de vérités sur l'expérience, peut elle être utile pour la connaissance expérimentale ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.