Re: Alerte crackpots

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.