Je ne sais pas quelle formation tu as eu, mais la question de la qualité dans le développement logiciel c'est loin d'être généralisé même aujourd'hui, que ce soit en entreprise ou dans les formations.
C'était une formation en logique mathématique et sur les fondements de l'informatique. Personnellement, à l'époque, la partie fondements de l'informatique ne m'intéressait pas spécialement. Je voulais surtout approfondir mes connaissances en logique et voir ce qu'avaient donné les attaques contre la philosophie kantienne des mathématiques (j'ai lu la Critique de la Raison Pure à la fin de ma spé, et je suis kantien depuis cette époque). Pour ceux intéressés par l'informatique, d'après la brochure sur les débouchés, il semblerait qu'ils finissent par faire une thèse et de la recherche (dans les organismes publiques ou en R&D chez des industriels genre EDF).
J'ai bien conscience qu'une telle formation est à part par rapport aux formations courantes des ingénieurs informaticiens.
Déjà, je dirais que pour être rigoureux intellectuellement, il faut démontrer que la solution proposée apporte quelque chose. Même si cela paraît évident. Car comme je l'ai dit, ce n'est pas parce que ton travail provient de la recherche universitaire que cela est forcément bénéfique. On ne va pas lister le nombre de prédictions théoriques de la recherche fondamentale (dont sur les noyaux de système d'exploitation) qui n'ont jamais su percer dans l'industrie faute d'adéquation en réalité.
Démontrer comment, par l'exemple ? Mais, de mon point de vue, un fait ne prouve pas grand chose : je m'intéresse surtout aux méthodes et à leur limite. Je suis un obsédé de la certitude : qu'est-ce que la certitude ? de quoi peut-on être certain ? quelles méthodes peuvent espérer atteindre à la certitude, lesquelles ne le peuvent pas ? font partie des questions qui m'obsèdent. Et de ce point de vue, l'induction et la méthode expérimentale reviennent à cela :
l'expérience ne donne jamais à ses jugements une universalité vraie et rigoureuse, mais seulement supposée ou comparative, si bien que cette universalité doit proprement signifier : Pour autant que nous l'ayons perçu jusqu'ici, il ne se trouve pas d'exception à telle ou telle règle.
Kant, introduction de la Critique de la Raison Pure.
ou pour citer Einstein résumant la philosophie sceptique de Hume : « l'empirique, dans la connaissance, n'est jamais certain (Hume) ». Il ne fut néanmoins pas convaincu par la réponse kantienne aux objections de Hume : « Kant propose alors une pensée. Sous la forme présentée elle est indéfendable mais elle marque un progrès nette pour résoudre le dilemme de Hume ». Pour ma part, je la trouve on ne plus défendable, et la méthode qu'il employa est analogue à celle utilisée par tous les systèmes de types des langages de programmations. Pour pousser le distinguo à l'extrême : je n'ai aucune certitude que le soleil se couchera se soir, mais je n'ai aucun doute quant à ce qu'exprime le théorème de Pythagore.
Pour revenir aux outils d'analyses et de sécurisation de code, il ne s'agit pas nécessairement de spécifier dans les moindres détails chaque bout de code et d'apporter la preuve du respect de la spécification, mais il est peut être envisageable d'ajouter certaines annotations en commentaires (à la manière de frama-c) pour avoir un système de type à l'expressivité plus riche que celui du C. Le système de type de C, de fait, exprime des spécifications sur le code mais, comme c'est peu ou prou la logique propositionnelle du premier ordre, on ne peut pas y exprimer grand chose : ce que fait le code et comment l'utiliser est beaucoup trop sous-spécifié avec un tel système de type.
Prenons un exemple. Je ne connaissais Coccinelle que de nom, je suis allé voir un peu leur site, et sur la page consacrée aux évolutions collatérales ils donnent deux exemple : ajout d'un argument à une fonction et changement dans le protocole d'initialisation des pilotes. Il semblerait que les pilotes aient mis un certain temps à s'adapter correctement à ce changement d'interface dans le cœur du noyau. Ces changements il faut bien les documenter quelque part ? Pourquoi pas dans une langue proche par sa syntaxe et son vocabulaire de l'anglais, mais à la grammaire plus régulière, et l'écrire en commentaire du code modifié ? On pourrait alors avoir une logiciel d'aide à l'audit qui détecterait automatiquement les mauvais usages des nouveaux codes.
Entre un audit totalement manuel et un audit partiellement automatisé, dans le monde de l'informatique ça doit pouvoir convaincre (pourquoi faire à la main ce qu'une machine peut faire pour moi ?). Je ne suis membre d'aucune des deux communautés (celle du noyau et celle de la recherche), mais je sais que la seconde est en état de fournir ce genre d'outil à la première. Néanmoins, pour cela, il faudrait une coopération et une synergie entre elles qui ne semblent pas exister aux dires de gasche. Je ne peux que trouver cela dommage.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Par contre, s'il y a un comportement indéfini du source, donc sémantique non définie, je pense pas que ça dise quoi que ce soit d'utile (on obtient juste un comportement « go wrong » accompagné d'une trace dès que la sémantique bloque, donc au mieux ça dirait peut-être que jusqu'au moment où ça bloque la sémantique est préservée).
C'est sur ce point que je ne sais pas ce qui est permis par le standard du C. Il y a des exemples de undefined behavior dans le manuel mais pas celle de l'exemple du journal : les exemples sont les overflow sur l'arithmétique signée (qui sont définies dans CompCert par les règles de l'arithmétique modulaire) et les accès hors bornes pour les tableaux qui renvoient une erreur.
D'après le deuxième principe que je cite du manuel « Second, the compiler is allowed to select one of the possible behaviors of the source program », le compilateur peut choisir n'importe quel comportement possible en accord avec la norme en cas de non déterminisme; c'est sur ce point que je n'ai pas bien compris si le choix de clang est acceptable (certains disent que oui, d'autres disent non) et pour moi cela reste encore bien obscur.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
La qualité du noyau (je dirais même la qualité logicielle au sens large), honnêtement, c'est assez récent comme problématique (moins de 5-10 ans), les choses se mettent en place et les progrès sont malgré tout importants.
Je suis étonné du caractère si récent de la prise en compte d'une telle problématique. J'ai terminé mes études il y a une quinzaine d'années et ce genre de questions étaient au cœur de la formation. Personnellement, l'utilité pour l'informatique était une chose qui, à l'époque, me semblait un cas d'application amusant mais sans plus; je regardais la chose d'un air amusé, les fondements des mathématiques m'important plus que ceux de l'informatique. Ce n'est que très récemment que je me suis repenché sur le lien avec le développement logiciel. À l'époque, les deux seuls langages que l'ont m'a enseigné était OCaml et Coq : avec le premier je m'étais amusé à faire un système de calcul formel sur l'arithmétique transfinie de Cantor, et avec le second j'avais formalisé quelques résultats élémentaires d'arithmétiques. Autant dire des questions de peut d'intérêt pour du développement logiciel.
Ceci étant dit, il est connu de longue date que la qualité logicielle relève de la preuve mathématique. Les approches dignes des sciences expérimentales à coup de tests unitaires ou de fuzzer, c'est gentil : ça peut détecter la présence de bugs, mais cela n'en prouvera jamais l'absence. À un moment, quand on affirme, il faut pouvoir prouver, quitte à le faire à la main :
Vous affirmez ? j'en suis fort aise.
Et bien ! prouvez maintenant.
pourrait être la devise des kantiens.
Quand je lis, par exemple, dans ce fil, que Nicolas Boulay demande qu'il faut démontrer la supériorité d'une solution avant de la mettre en œuvre et que gasche doit lui répondre :
Ce dont je parle ici (mais c'est loin d'être la seule sorte de recherche qui pourraitêtre utile au noyau) c'est d'éliminer, par des outils d'analyse, des classes entières de bugs possibles du code du noyau (use-after-free, accès à de la mémoire non initialisée, usage incorrect des verrous…). Tu écris comme si l'utilité de ce résultat final restait à démontrer, ce qui me semble complètement fou—évidemment c'est utile, et évidemment un noyau qui a su mettre ces outils en place va se retrouver loin devant un noyau qui ne l'a pas fait sur le long terme, en terme de robustesse et de qualité.
je tombe des nues. :-O Mais enfin, c'est une évidence pour qui est un minimum rigoureux intellectuellement ! On pourrait y rajouter en écho ce passage de l'évangile selon Saint Luc (chapitre 6, versets 47-49) :
47 Quiconque vient à moi, écoute mes paroles et les met en pratique, je vais vous montrer à qui il ressemble.
48 Il ressemble à celui qui construit une maison. Il a creusé très profond et il a posé les fondations sur le roc. Quand est venue l’inondation, le torrent s’est précipité sur cette maison, mais il n’a pas pu l’ébranler parce qu’elle était bien construite.
49 Mais celui qui a écouté et n’a pas mis en pratique ressemble à celui qui a construit sa maison à même le sol, sans fondations. Le torrent s’est précipité sur elle, et aussitôt elle s’est effondrée ; la destruction de cette maison a été complète. »
ou encore cet extrait de la préface des Prolégomènes à toute métaphysique future qui pourra se présenter comme science de Kant :
D'autre part il n'est pas tellement inouï qu'après avoir longtemps pratiqué une science, si on pense avec étonnement au progrès qui y a été accompli, on finisse par se poser la question de savoir si et comment de façon générale une telle science est possible. Car la raison humaine est assez désireuse de construire pour qu'il lui soit déjà maintes fois arrivé de bâtir la tour pour, puis de la démolir pour voir de quelle nature pouvait bien être son fondement. Il n'est jamais trop tard pour devenir sage et raisonnable; mais lorsque l'enquête est tardive, elle est plus difficile à mettre en train.
Lorsque gasche affirme que c'est un investissement sur le long terme :
Long terme: je pense que si les gens s'y mettaient sérieusement aujourd'hui il faudrait de l'ordre de 10-15 ans pour ça porte ses fruits.
cela va également de soi. Mais plus le projet tarde à s'y mettre, plus la base de code (déjà très volumineuse) augmentera et plus il sera difficile, voire surhumain, de mettre en pratique ce genre d'approche de contrôle qualité. Il vient donc naturellement à l'esprit cette question : la communauté en charge du développement du noyau est-elle sensible à ces questions ou s'en moque-t-elle fondamentalement ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Autant le code python me parle (je ne connais pas du tout ce langage), autant le DSL ne me parle pas.
Là, il y à un truc que je ne comprends pas du tout. Je n'avais pas prêté attention au message de ta part auquel gasche t'a répondu en présentant ce DSL, mais tu y reprochais à OCaml de ne pas générer des instructions SIMD en écrivant :
De plus, ocaml pourrait faire des map et fold sur des array de nombres, et proposer des versions vectorisés des opérations en question.
Il te répond avec un langage qui fait cela pour du code sur GPU, et tu réponds que ça ne te parle pas ? C'est quoi le problème ? Qu'ils utilisent la lettre pour définir des fonctions ? Qu'ils écrivent reduce et non fold ?
L'incompréhension venait du fait que le message de Renault pouvait être compris comme : « à partir de -O2 le compilateur se réservait le droit de modifier la sémantique d'un programme [qui possède une sémantique] ».
Tu n'es pas très joueur ! Moi, quand je m'ennuie, je joue à la roulette russe; ou en plus fun, je fais comme cap'tain sports extrêmes : je fais du saut à l'élastique mais sans élastique, avec un élastique on a aucune sensas' ! :-P
Pour prendre le manuel d'un compilateur qui ne s'amuse pas à changer la sémantique du code (« Traduttore, traditore » ou « Traducteur, traître » dit son manuel) :
There are three noteworthy points in the statement of semantic preservation above:
[…]
Second, the compiler is allowed to select one of the possible behaviors of the source program. The C language has some nondeterminism in expression evaluation order; different orders can result in several different observable behaviors. By choosing an evaluation order of its liking, the compiler implements one of these valid observable behaviors.
Third, the compiler is allowed to improve the behavior of the source program. Here, to improve means to convert a run-time error (such as crashing on an integer division by zero) into a more defined behavior. This can happen if the run-time error (e.g. division by zero) was optimized away (e.g. removed because the result of the division is unused). […]
et à la question « qu'est-ce qu'un comportement observable ? », il précise :
More precisely, we follow the ISO C standards in considering that we can observe:
Whether the program terminates or diverges (runs forever), and if it terminates, whether it terminates normally (by returning from the main function) or on an error (by running into an undefined behavior such as integer division by zero).
All calls to standard library functions that perform input/output, such as printf() or getchar().
All read and write accesses to global variables of volatile types. These variables can correspond to memory-mapped hardware devices, hence any read or write over such a variable is treated as an input/output operation.
Je ne connais pas bien la sémantique du C mais, pour l'exemple du journal, il me semble bien que l'optimisation de clang ne respecte pas ces principes.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Ceci est à mettre en parallèle avec les énoncés que l'on ferait sur l'encodage des entiers naturels dans ZF, où on écrirait pour énoncer une propriété des entiers. Ici le quantificateur universel sur x parcourt la collection de tous les ensembles (intreface{}) puis l'énoncé est une proposition hypothétique dont l'antécédent correspond à une vérification dynamique de type avant de continuer « l'exécution » vers le conséquent.
Et ça marche !! :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Au passage, je me demande s'il n'y a pas un lien avec une autre entrée de suivie que j'avais faite. Quand on met plusieurs formules en lignes et que l'on mélange avec du texte en chasse-fixe, elles ne sont pas toutes traitées.
Un test : le (d'où le \ de Haskell ou Elm) du lambda-calcul était à l'origine en majuscule .
Je veux bien essayer de voir d'où cela vient et tenter de corriger le problème, mais je ne sais pas par où commencer dans la base de code du site.
P.S : après prévisualisation, le test semble bien traiter le , mais ce n'est pas toujours le cas. Dans ce commentaire, j'ai un $x \in \omega$ non interprété en .
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
La non constructivité induit qu’il n’existe pas forcément de moyen de former un algorithme à partir du théorème ou de la formule, et c’est bien tout…
La correspondance s'étend aussi au raisonnement par l'absurde et donc à la logique classique, ce sont les exceptions dans les langages de programmation (les blocs try-with-finally). Voir ce texte de Jean-Louis Krivine (page 3).
Je crois que tu confonds « formule de la logique du premier ordre » et « logique du premier ordre ». Ou alors c’est moi qui confond…
Ce n'est qu'une question de vocabulaire : il y a d'un côté les jugements que l'on considère (calcul des prédicats ou calcul propositionnel, au premier ou second ordre) et de l'autre les règles de déductions (classique ou intuitionniste). Comme dans une logique on considère à la fois les règles de formations des jugements et les règles de déduction, pour éviter toute ambiguïté, il serait sans doute préférable de parler de logique classique du premier ordre et de logique intuitionniste du premier ordre.
Cela dit j’ai quand même l’impression d’être grugé. Dans un cas, le connecteur « -> » est vu par correspondance de curry-howard comme le type d’une fonction, alors que dans l’autre pour un langage dynamique tu as complètement oublié cette correspondance implication/fonction et c’est le quantificateur qui joue ce rôle.
Le quantificateur universel c'est le du lambda-calcul, le\ de Haskell, le fun de OCaml… c'est lui qui abstrait sur la totalité d'un domaine et, effectivement, dans le calcul des prédicats, on abstrait sur tout le domaine du modèle — sur tout l'univers des ensembles dans ZF. Les langages dynamiques sont des langages avec typage statique… qui n'ont qu'un seul type statique. Là où dans les théories des types, comme en Coq, on peut n'abstraire que sur les valeurs d'un type donné.
L'implication est bien toujours le signe d'une fonction mais, dans mon exemple, elle ne spécifie rien sur sa sortie pour une entrée qui n'est pas un ordinal. Si on reprend mon énoncé (légèrement modifié) :
il dit qu'à tout ensemble x, il peut en associer un autre y. Lorsque x est un ordinal, l'énoncé affirme que y est son prédécesseur qui est aussi un ordinal, mais dans le cas contraire (qui peut arriver, on a quantifié sur tous les ensembles), il ne dit rien sur y. La preuve d'un tel théorème expose, dans le cas où x est un ordinal, un moyen de produire un tel y et fournit la preuve que y est aussi un ordinal. En revanche, dans le cas où x n'est pas un ordinal, elle ne dit rien sur y (si ce n'est que c'est un ensemble, donc n'importe quelle valeur possible). Ce qui me fait penser à ce code Go :
funcpred(vinterface{})(uint,error){varresuintvarerrerrorswitchi:=v.(type){caseuint:ifi==0{res=uint(0)}else{res=uint(int(i)-1)}default:err=errors.New("not an uint")}returnres,err}
Il prend en entrée toute valeur possible (n'importe quel ensemble pour ZF), dans le cas où c'est un uint renvoie un y selon la même spécification que l'énoncé, ou bien renvoie une erreur si l'entrée n'est pas de type uint (cas de la preuve qui ne dit rien sur y, on renvoie une erreur). Ici le procédé est totalement constructif au sens des règles de déductions intuitionnistes. Le fait que la preuve du théorème prouve aussi que y est un ordinal, quand x l'est, se retrouve sur le type de sortie de la fonction en Go.
Après réflexion, on pourrait faire quelque chose de similaire en OCaml. Pour cela, il faut un type dans lequel on puisse plonger des valeurs de n'importe quel type : on parle de type universel. La signature d'un module fournissant un tel type est :
Je passe les détails d'implémentations d'un tel module (il faut utiliser un type somme extensible, comme l'est celui des exceptions dans le langage) et montre juste son usage en supposant que l'on a module U : Univ, c'est à dire un module fournissant un tel type :
(* ici on a des fonctions pour injecter dans et projeter * depuis le type `U.t` des valeurs de type `int` ou `nat` *)let(inj_int:int->U.t),proj_int=U.embed()let(inj_nat:nat->U.t),proj_nat=U.embed()(* on définit maintenant à partir de la fonction `pred` sur `nat` * une fonction `pred` générique sur le type universel `U.t` *)letpred_genv=matchproj_natvwith|None->None|Somen->Some(predn);;valpred_gen:U.t->natoption=<fun>(* si la valeur de type `U.t` contient un `int`, on renvoie `None` *)pred_gen(inj_int2);;-:natoption=None(* si elle contient un `nat`, on renvoie son prédecesseur *)pred_gen(inj_nat(S(SO)));;-:natoption=Some(SO)
Pour en revenir aux différentes logiques, le problème est bien dans le calcul des prédicats. Il est tel que, lorsqu'on l'interprète, toute les choses dont il parle sont considérées comme étant homogènes. Par exemple, si on veut formaliser la théorie des espaces vectoriels dans un tel symbolisme, il faut mettre les scalaires et les vecteurs dans un même sac fourre-tout et un modèle d'une telle théorie devra donner une signification à la somme d'un scalaire et d'un vecteur (ce qui, fondamentalement, n'a aucun sens dans un tel cadre). Raison pour laquelle je disais que les approches de la logique via la théorie des types captent bien mieux la notion de concept : le concept de scalaire ne sera nullement mélangé arbitrairement avec celui de vecteur, ce seront deux types distincts.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Je suis ingénieur, et je n'avais pas entendu parler de Lambda avant de faire un dea d'info.
Moi aussi, je n'avais jamais entendu parler de lambda-calcul avant mon DEA. Ce que je voulais dire, dans le fond, c'est que le niveau d'abstraction requis pour le comprendre relève du premier cycle en mathématique (une fois que l'on a expliqué ce que signifie le lambda, ce qui prend deux minutes). Tu trouves (si je me fie à ce que j'ai déjà lu) que elm est un bon langage pour faire du développement web : ce type de code doit être assez standard en elm. Elm a la même syntaxe que Haskell où le lambda est remplacé par l'anti-slash \, c'est tout. Après c'est du map-reduce, on ne peut plus classique en programmation fonctionnel, ce qui n'exige pas un niveau de compréhension d'un niveau doctoral.
En OCaml, on l'écrirait ainsi :
(* reduce c'est tout simplement fold_left *)letreduce=List.fold_left(* opérateur de composition infixe *)let(<.>)fg=funx->f(gx)letmap=List.mapletzip=List.combineletmul(a,b)=a*bletsum=reduce(+)0(* le lambda c'est le mot-clé fun *)letdot=funxsys->(sum<.>mapmul)(zipxsys)dot[1;2][3;4];;-:int=11
L'avantage pour des chercheurs de passer par du lambda-calcul, sans ajouter trop de sucre syntaxique, est d'avoir rapidement un prototype opérationnel comme preuve de concept.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
J'imagine que les usagers de ce genre de DSL sont docteur en mathématique pour le calcul linéaire. Je ne vois pas qui d'autres pourraient s'en servir vu le formalisme mathématique retenu.
Tu ne penses pas que tu exagères un peu là ? C'est du niveau premier cycle en mathématique (allez, fin de premier cycle pour être gentil).
la différence étant que les fonctions map n'ont pas la même interface entre les deux langages. La définition du produit scalaire entre vecteurs en python, je l'ai prise de la documentation python officielle. Sinon, voir aussi cette réponse sur stackoverflow :
Je précise ici ma réponse sur ZF vu comme un langage dynamiquement typé. On pourra continuer la discussion de cette sous-question sous ce commentaire et laisser celle sur la physique à un autre fil.
Je comprend bien l’idée, mais l’analogie trouve ses limites vu que la logique du premier ordre n’est pas constructive.
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. J'ai déjà écrit ailleurs un commentaire, en réponse à une question de Michaël, sur la différence entre les deux notions, le rapport entre programmes et preuves de théorème (correspondance de Curry-Howard) et la distinction entre les systèmes de types de OCaml et de Coq.
Si x n’appartient pas à Oméga, ben, rien, ça ne pose pas de problème.
Si ça pose problème : dans un cas l'énoncé est prouvable dans ZF (c'est un théorème) dans l'autre il est réfutable, et cela selon les règles intuitionnistes (sans raisonnement par l'absurde). Exemples :
Le premier se paraphrase en français ainsi : tout ordinal fini est soit vide, soit le successeur d'un ordinal fini. Le second se paraphrase ainsi : tout ensemble est soit vide, soit le successeur d'un autre. Tu remarqueras, au passage, que le français est tout à fait apte à exprimer de tels énoncés, sans recourir à un symbolisme quelconque. ;-)
Le premier est trivialement vrai, le second est trivialement faux dans ZF. Le premier exprime le type de la fonction prédécesseur. En OCaml, on écrirait cela ainsi :
En Coq, cela se formalise de manière assez similaire :
InductiveNat:=|O:Nat|S:Nat->Nat.Fixpointpredx:=matchxwith|O=>O|Sn=>nend.(* j'y adjoins la preuve du théorème *)Theorempred_spec:forall(n:Nat),n=O\/exists(m:Nat),n=Sm.Proof.intron.destructn.-left;reflexivity.-right;existsn;reflexivity.Qed.
Ici la fonction pred est sous-spécifiée (elle a pour type Nat -> Nat), mais on pourrait lui donner un type plus précis analogue à ce qu'exprime le théorème, qui est la traduction en Coq du premier énoncé pour ZF. En revanche les contraintes de typage statique de l'un ou l'autre langage ne permettent pas d'exprimer le second énoncé. Contrairement à Python :
>>>defpred(x):...iftype(x)==int:...ifx==0:...return0...else:...returnx-1...else:...return"not an int"...>>>pred(2)1>>>pred("a")'not an int'>>>pred_unsafe=lambdax:x-1>>>pred_unsafe("a")Traceback(mostrecentcalllast):File"<stdin>",line1,in<module>File"<stdin>",line1,in<lambda>TypeError:unsupportedoperandtype(s)for-:'str'and'int'
La fonction pred avec vérification dynamique de type s'apparente au premier énoncé, tandis que la seconde fonction pred_unsafe s'apparente au second.
J'espère que la chose te semble plus claire maintenant. Il vaudrait mieux, du moins, car c'est une promenade de santé par rapport au problème du rapport entre le kantisme et ce qu'il entend par réalité. Ma réponse à ce sujet viendra plus tard, peut être ce midi ou en fin de journée si je trouve le temps qu'il faut pour la rédiger.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Cela dit si tu ne postules pas ça, il ne peux y avoir de sciences.
Les kantiens n'ont jamais nié une telle chose.
Je comprends pas trop en quoi tu postules que je veux me débarrasser de l’observateur.
Bah, quand on me dit que la pierre a une existence propre spatio-temporellement déterminée, j'interprète cela comme abstraction faite de tout rapport à un observateur possible, c'est-à-dire que l'on se débarrasse de l'observateur. Autrement dit, qu'il y est ou non des hommes, il existe un monde dans lequel des pierres évoluent dans l'espace et le temps et la physique est là pour découvrir les lois d'un tel monde. Ce que disent les kantiens, ce n'est rien d'autre que ce que disait Socrate : nous ne voyons que des ombres sur un mur, tels les esclaves de l'allégorie de la caverne. Qu'il y est quelque chose qui nous apparaisse comme une pierre spatio-temporellement déterminée, que cette chose soit bien réelle, nous l'accordons; nous disons juste qu'elle n'est telle que pour les êtres humains.
Je te répondrai plus en détail demain, mais j'ai l'impression que tu te méprends (comme Einstein lui-même d'ailleurs) sur ce que veulent dire les kantiens quand ils affirment que la pierre (ou tout autre objet physique) ne sont pas des choses en soi existant « sans nous ».
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 …
Disons que sans écrire un énoncé à quantificateur universelle borné (la condition ), on risque la contradiction ou l'énoncé vide de sens. ;-)
C’est une notion logique la notion de concept ?
Un peu mon neveux ! La logique s'occupe des règles pour former des concepts, des règles pour former des jugements à partir de ces concepts et des règles pour enchaîner ces jugements entre eux ou raisonnements. Le plan de la doctrine générale des éléments du traité sur la logique de Kant :
Des concepts
Des jugements
Des raisonnements
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
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.
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).
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. Deuxièmement, 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; et 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 pourrais développer ce point en faisant une analyse comparée d'un texte d'Enstein (un article qu'il a écrit sur Bertand Russel) et de la plaidoirie de Kant pour se défendre d'être un idéaliste (au sens que ce terme à en philosophie), si tu souhaites plus de précisions. La plaidoirie de Kant est, dans le fond, une réponse à l'objection que tu m'opposes.
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 « É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.
Ton interprétation (libre) ne tombe pas loin de la réalité : telle était l'intention primordiale de la théorie, mais c'est « mal » fait. L'idée étant de voir un ensemble comme un concept dont l'extension (la totalité de ses éléments) dénote les objets tombant sous le concept (d'où, par exemple, l'axiome d'extensionnalité affirmant que deux ensembles ayant les mêmes éléments sont égaux), et l'inclusion entre ensembles exprimant alors la subordination entre concepts, c'est-à-dire du sous-typage.
Ma comparaison avec le typage dynamique (comparaison à laquelle j'ajoutais si je peux m'exprimer ainsi) vient du fait que lorsque l'on prend un énoncé universellement quantifié de la théorie, on quantifie sur tout l'univers des ensembles qui se comporte alors à la manière du interface{} du Go. ;-) Raison pour laquelle les auteurs de HoTT écrivent en introduction de leur ouvrage :
In type theory, unlike set theory, objects are classified using a primitive notion of type, similar to the data-types used in programming languages. […]
This rigidly predictable behavior of all objects (as opposed to set theory’s more liberal formation principles, allowing inhomogeneous sets) is one aspect of type theory that has led to its extensive use in verifying the correctness of computer programs.
Ce que j'ai graissé est à mettre en lien avec les reproches adressées à Go d'utiliser le interface{} pour la généricité du code, ce qui ne permet pas de garantir statiquement l'homogénéité d'une liste : il faut écrire des fonctions de constructions qui font du typage dynamique à base de switch sur les types des paramètres.
Ceci est à mettre en parallèle avec les énoncés que l'on ferait sur l'encodage des entiers naturels dans ZF, où on écrirait pour énoncer une propriété des entiers. Ici le quantificateur universel sur x parcourt la collection de tous les ensembles (intreface{}) puis l'énoncé est une proposition hypothétique dont l'antécédent $x \in \omega$ correspond à une vérification dynamique de type avant de continuer « l'exécution » vers le conséquent. 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. En Coq ou en HoTT, on écrirait tout simplement forall (x : Nat) ..., soit pour tout entier, .... La notion de type capture bien mieux que celle d'ensembles (au sens de ZF) la notion logique de concept.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
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 ;).
Ce que tu me demandes (infirmer la chose) est impossible à effectuer dans un commentaire. Tout ce que je peux dire c'est que les liens entre la philosophie kantienne et les théories des types contemporaines sont une évidence pour qui les connaît : elles procèdent toutes de la même approche méthodologique.
Le mieux que je puisse faire dans un commentaire, c'est pointé du doigt quelques références : Per Martin-Löf et Jean-Yves Girard.
Le second est l'auteur, entre autre, du système F qui est un système de types génériques pour le lambda-calcul : c'est le système de type à la base de langages comme Haskell ou OCaml. Sur sa page personnelle (le lien est sur son au-dessus) tu trouveras une partie intitulée La syntaxe transcendantale :
La syntaxe transcendantale est la justification technique des thèses du fantôme de la transparence. Le programme est exposé dans l'article La syntaxe transcendantale, manifeste (Février 2011).
Le livre en question (le fantôme de la transparence) est celui dont j'ai parlé à gasche dans ce commentaire. Je ferais deux remarques là-dessus. Le qualificatif transcendantale est une référence on ne peut plus explicite à Kant, ce dernier ayant utilisé les expressions philosophie transcendantale ou philosophie critique pour qualifier son œuvre philosophique. Ensuite, à la fin de l'introduction du livre, on peut lire :
Le principal bénéficiaire de cette visite non guidée aura été l'auteur, tout surpris d'y trouver matière à de futurs développements techniques. Et de découvrir la surprenante adéquation du kantisme — au sens large — à la logique contemporaine. Ce qui n'est pas très étonnant après tout : que veut dire « raison pure », sinon logique ?
En ce qui concerne Martin-Löf, il est également l'auteur d'une théorie de types dépendants intuitionnistes. Il a participé au groupe de travail ayant écrit la théorie homotopique des types (HoTT) visant à fournir une alternative à ZF pour le fondement des mathématiques basée sur la théorie des types (ça se comprend, ZF c'est l'archétype du typage dynamique; il n'y a qu'un seul type statique : celui d'ensemble, tout le reste est dynamique, si je peux m'exprimer ainsi). Dans l'introduction du livre HoTT, on lit :
Per Martin-Löf, among others, developed a “predicative” modification of Church’s type system, which is now usually called dependent, constructive, intuitionistic, or simply Martin-Löf type theory. This is the basis of the system that we consider here; it was originally intended as a rigorous framework for the formalization of constructive mathematics.
Lorsque l'on s'occupe à notre époque de théorie des types, éluder toute référence kantienne pourrait s'apparenter, pour reprendre une expression utilisée ailleurs dans les commentaires, à une faute professionnelle.
Kant et la physique théorique
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 …
Je n'ai pas écouté la conférence mais seulement lu le texte qui l'accompagne. Je ferais deux remarques là-dessus :
l'auteur occupe la chaire de psychologie cognitive expérimentale ;
le terme « hypothèse » revient à de nombreuses reprises, comme il se doit pour une science expérimentale.
Kant et les kantiens ne pratiquent pas de science expérimentale mais de la science pure ou rationnelle, c'est-à-dire des sciences dont les principes fondamentaux ne sont pas fondés sur l'expérience et l'observation, et dans les sciences expérimentale ne considèrent que la forme nécessaire que doivent prendre leurs théories pour être adéquate à la structure de notre esprit. Tu noteras que je parles d'esprit et non de cerveau : le cerveau est aussi peu le siège de la pensée que le cœur est celui des émotions, si ce n'est par amalgame matérialiste. Dans un tel champ du savoir, le recours aux hypothèses est mal venu :
Pour ce qui concerne la certitude, voici la loi que je me suis imposée à moi-même : dans cette sorte de considération, l'opinion n'est en aucune façon permise, et tout ce qui ressemble seulement à une hypothèse est une marchandise prohibée, qui ne doit pas être mise en vente à bas prix, mais doit être saisie aussitôt que découverte. Car toute connaissance qui doit être établie a priori donne d'elle même à entendre qu'elle veut être tenue pour nécessaire; plus encore en ira-t-il d'une détermination de toutes les connaissances pures a priori, qui doit être la mesure et par la même l'exemple de toute certitude apodictique (philosophique).
Kant, Critique de la Raison Pure.
Avoir recours à des hypothèse dans ce genre d'enquête, ce serait comme vouloir fonder la mathématique sur des conjectures : ce n'est pas sérieux.
Maintenant, comme exemples de personnes ici du monde de la physique ayant écouté l'appel de Kant, je citerai :
Thibault Damour membre de l'académie des Sciences et spécialiste de relativité générale, d'après son texte sur la question Le temps passe-t-il ? (voir page 9)
des épistémologues et physiciens d'après la conclusion du livre Petit voyage dans le monde des quanta d'Étienne Klein :
Certes les problèmes de fond posés par Bohr, Heinsenberg, Einstein, Schrödinger ou Pauli restent d'actualité, mais on dispose aujourd'hui pour les traiter de davantage de résultats et de davantage d'arguments. Plusieurs systèmes épistémologiques essaient d'intégrer ces nouvelles donnes : la thèse du réel voilé de Bernard d'Espagnat, le solipsisme convivial d'Hervé Zwirn, le réalisme physique de Michel Paty, et de façon plus diffuse le réalisme ouvert, l'opérationnalisme, le phénoménalisme, et enfin l'idéalisme, lui-même divisé en idéalisme radical et idéalisme modéré, les deux pouvant être plus ou moins kantiens…
E. Klein, Petit voyage dans le monde des quanta.
J'ajouterai simplement qu'une telle situation n'a rien d'étonnant quand on connaît certaines résultats de la physique quantique et le contenu de la philosophie kantienne. Je conclurai sur la réponse d'un kantien à un extrait du livre d'Étienne Klein :
En premier lieu, s'il est vrai que le vecteur d'état contient tout ce que l'on peu savoir d'un système quantique, autrement dit si le formalisme est complet, il faut admettre qu'un phénomène ne peut être interprété comme fournissant des informations concernant des propriétés qu'auraient les objets eux-mêmes, indépendamment de la connaissance que nous en avons. Songeons à une pierre. C'est un objet qui existe « pleinement » au sens où nous n'hésitons pas à lui attribuer par la pensée des propriétés bien définies : une taille, une forme, une couleur qui sont ce qu'elles sont, même en l'absence d'observateur. Les objets quantiques, eux, ne semblent pas pouvoir être considérés de la sorte puisque leurs propriétés ne sont pas toujours déterminées antérieurement à la mesure qui en est faite.
Ce qui choque un Kantien n'est pas ce qu'il dit des objets quantiques, mais ce qu'il dit de la pierre ! :-P
Les objets que nous observons, en tant qu'objets de la connaissance expérimentale, n'ont aucune existence propre indépendante de nous. Si nous voyons partout de l'espace et du temps dans l'expérience, c'est parce qu'on les y met nous-même (voir l'article de Thibault Damour). Ainsi, lorsque l'on fait abstraction de tout rapport à l'expérience possible alors l'espace et le temps s'évanouissent, ce qui nous apparaît comme une pierre dans l'expérience devient un quelque chose d'inconnu, qui nous restera à jamais inconnaissable, une chose ineffable (dont on ne peut parler). L'avantage du kantisme sur toute autre approche épistémologique est qu'il ne fait aucune distinction ontologique entre la pierre et les objets quantiques : ce ne sont que de simples phénomènes qui n'ont pas d'existence propre en dehors de leur rapport à un observateur.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Il y a quand même une légère différence dans les détails :)
Pas spécialement, le principe que je décris est celui qu'a utilisé Gödel pour démontrer son fameux théorème d'incomplétude : une théorie assez riche (au pouvoir expressif suffisant) pour parler d'elle même a toujours des énoncés indécidables (qu'elle ne peut ni prouver ni réfuter) et parmi ceux-ci figurent toujours sa propre cohérence (sa non contradiction). Ce que je dis c'est que si une théorie est assez riche (comme l'est ZF) pour exprimer les principes de la théorie des modèles et donc parler de la relation entre la forme et le contenu (ce en quoi consiste la vérité) alors elle ne peut engendrer son propre contenu (elle ne peut construire un modèle d'elle même) et fournir un critère matériel et universelle de la vérité, sous peine d'être incohérente d'après le théorème d'incomplétude. Dans ce cas, comme elle peut prouver tout et n'importe, on ne peut nullement avoir confiance dans ce qu'elle prétend affirmer.
Cette démarche consiste à réfléchir la métathéorie dans la théorie elle même, c'est le même genre d'argument qu'a utilisé Turing pour prouver l'impossibilité de résoudre le problème de l'arrêt pour sa machine universelle. D'un point de vue programmation, cela revient à dire qu'un langage ne peut se compiler lui-même sans une phase de bootstrap : il faut un coup de pouce extérieur au langage de programmation.
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.
L'univers des constructibles de Gödel sert à prouver des théorèmes de consistance relative : si ZF est non contradictoire alors il en est de même de ZF augmentée de l'axiome du choix, ce dernier axiome n'introduit pas de contradiction dans la théorie. C'est du même ordre que les théorèmes de consistance relative que Poincaré a effectués au XIXème entre les géométries euclidienne et non euclidiennes. Le cercle de Poincaré, construit dans un espace euclidien, permet d'interpréter les axiomes de la géométrie hyperbolique. Autrement dit, si la géométrie euclidienne est cohérente alors il en est de même de l'hyperbolique.
En revanche aux questions : l'arithmétique est-elle cohérente ? la géométrie est-elle cohérente ? ZF est-elle cohérente ? la logique et son principe de contradiction est incapable d'y répondre. La seule chose qu'elle peut faire c'est prouver la cohérence d'une théorie en admettant la cohérence d'une autre. Par exemple, on peut prouver la cohérence de l'arithmétique à partir de ZF, mais reste la question : ZF est elle cohérente ? On peut continuer en ajoutant des axiomes de grands cardinaux qui prouvent la consistance de ZF (ils fournissent un modèle de celle-ci), mais reviens alors la question : ses nouveaux axiomes sont-ils cohérents ? Et cette approche turtles all the way down la logique formelle ne peut en sortir, pour la simple raison que, laissée à elle même, elle n'engendre que des tautologies (l'art de M. de La Palice) et est incapable de répondre à la question : comment des jugements synthétiques a priori sont-ils possibles ?
Les principes abstraits en langage naturel de Kant se reflètent dans les méthodes formelles modernes. Mais enrichis :)
Ça se discute, ils ne sont nullement enrichis, ce sont les mêmes mais exprimés dans une langue différente. Un principe ne deviendrait ni plus vrai, ni plus clair, ni plus riche sous prétexte qu'il serait exprimés en français plutôt qu'en anglais (ou vice versa). La méthode kantienne est on ne peut plus formelle (il n'y a pas plus formaliste qu'un kantien), et les langues naturelles sont tout à fait adaptées pour exprimer de tels principes. Il n'est pas nécessaire de recourir à des symbolismes compréhensibles par une machine (ce qui n'est d'ailleurs adapté qu'à la formalisation de la pensée mathématique mais nullement à la pensée philosophique, comme les problèmes de philosophie du droit) pour formaliser sa pensée : je préfère de loin l'usage du français à Coq, par exemple. Les langues naturelles ont, en leur sein, un système à type dépendant mais une grammaire plus complexe que les grammaires régulières des langages de programmation (il suffit de voir la difficulté que rencontre l'auteur de grammalecte, ou tous ceux qui travaillent sur le traitement automatique des langues).
Prenons, un principe de base de la logique de Hoare utilisée pour la formalisation des langages impératifs, celui de la composition des instructions :
{ P } S { Q } { Q } T { R }
----------------------------
{ P } S ; T { R }
une expression de la forme { P } S { Q } se lit : l'instruction S fait passer le système de l'état P à l'état Q. Une telle règle ce lit alors : si l'instruction S fait passer la machine de l'état P à l'état Q et que l'instruction T fait passer de l'état Q à l'état R, alors la série d'instructions S ; T fait passer de l'état P à l'état R.
Il se trouve que c'est l'analogue dans le paradigme de la programmation fonctionnelle pure de la composition des fonctions :
funfgx->g(fx);;-:('a->'b)->('b->'c)->'a->'c=<fun>
A --> B B --> C
------------------
A --> C
Autrement dit, des deux prémisses si A alors B et si B alors C, on conclue à si A alors C. Cela résulte d'une double application de la règle dite du modus ponens :
si A alors B, or A donc B (modus ponens utilisant la première prémisse et l'hypothèse A)
si B alors C, or B donc C (modus ponens utilisant la seconde prémisse et la conclusion du syllogisme hypothétique précédent)
ainsi en supposant A on conclue à C, c'est à dire que l'on a prouvé si A alors C. Ce genre de preuve, quelque peu pédante, est ce que nous oblige à écrire Coq (il offre quand même des techniques pour éviter de rentrer autant dans les détails).
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 et qu'il a pour type (là j'emploie une terminologie contemporaine) la forme logique des jugements hypothétiques (si A alors B).
On pourrait exprimer le principe fondamentale de la dynamique de Newton ainsi dans un tel symbolisme : { p } F { p + F * dt}. Autrement dit, un corps dans l'état de mouvement p et soumis à une force F se retrouve dans l'état { p + F * dt } au bout d'un temps infiniment petit dt. L'on retrouverait ainsi les considérations entre les sémantiques petit pas (small step) ou grands pas (big step), auxquelles gasche faisait allusion dans ce commentaire, et la distinction entre les lois différentielles et les lois intégrales en physique théorique. La première étant une approche discrète (sémantique des langages de programmation), là où la seconde est continue (physique théorique).
Et c'est ce lien formel entre le principe de causalité et la forme des jugements hypothétiques qui explique que l'on peut construire des machines qui « exécutent » les calculs automatiquement.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
La logique peut aussi vérifier la cohérence interne des connaissances des experts sur leur sujet. […] Mais du point de vue de la cohérence, ça peut lever des lièvres.
Oui car telle est son affaire, elle peut montrer l'incohérence d'une formalisation. Pour ce qui est de prouver la cohérence, par contre…
Ça me rappelle ce passage humoristique dans la partie remerciements de la thèse de Perthmâd (qui, s'y j'en crois les notes de publication de la toute récente dernière version de Coq, a fait un gros travail de nettoyage et d'optimisation du langage des tactiques) :
— Un thésard demanda à Hugo Herbelin : « Coq est-il cohérent ? »
— Anomaly: Uncaught exception Mu.
Par malheur, l’histoire omet de raconter si l’étudiant fut illuminé ou bien s’il l’était déjà à l’instant même où il songea à passer un doctorat d’informatique fondamentale 5 [1].
[1]Par contre, l’histoire précise bien que le rapport de bug qui s’en suivit fut marqué WontFix par un certain kgoedel. Ce n’est pas dans le privé qu’on verrait ça.
Dans une démarche également historique, le passage que j'ai cité de la Critique de la Raison Pure est extrait du paragraphe sur la question « Qu'est-ce que la vérité ? » qui commence ainsi :
La vielle est célèbre question, par laquelle on se figurait pousser les logiciens dans leur retranchement et on cherchait à les amener, ou à devoir se laisser surprendre dans un pitoyable diallèle, ou bien à devoir avouer leur ignorance, et par la suite la vanité de tout leur art, est celle-ci : Qu'est-ce que la vérité ? La définition nominale de la vérité, qui en fait la conformité de la connaissance avec son objet, est ici accordée et supposée; mais on veut savoir quel est le critère universel et sûr de la vérité de toute connaissance.
C'est déjà une grande et nécessaire preuve de sagesse et de pénétration que de savoir ce que l'on doit raisonnablement demander. En effet, si la question est absurde en soi et si elle appelle parfois, outre la confusion de celui qui la soulève, l'inconvénient de porter à des réponses absurdes l'auditeur qui n'est pas sur ses gardes, et de donner ainsi le ridicule spectacle de deux personnes, dont l'un trait le bouc (comme disaient les anciens), tandis que l'autre tend un tamis.
Si la vérité consiste dans l'accord d'une connaissance avec son objet, cet objet doit être par là distinguer des autres; car une connaissance est fausse, si elle ne s'accorde pas avec lequel elle est rapportée, alors même qu'elle pourrait bien valoir pour d'autres objets. Or, un critère universel de la vérité serait celui qui vaudrait pour toutes les connaissances, sans distinction de leurs objets. Mais il est clair, puisqu'on y fait abstraction de tout contenu de la connaissance (du rapport à son objet), et que la vérité à trait justement à ce contenu, qu'il est tout à fait impossible et absurde de demander une marque de la vérité de ce contenu des connaissances, et qu'on ne peut donc proposer une caractéristique suffisante et en même temps universelle de la vérité. Comme nous avons déjà nommé plus haut le contenu de la connaissance sa matière, on devra dire : On ne peut demander aucune caractéristique universelle de la vérité quant à sa matière, parce que c'est en soi contradictoire.
Kant, Critique de la Raison Pure.
On trouve des considérations identiques dans le traité qu'il consacra à la logique. Premièrement, ce qu'il appelle la définition nominale de la vérité est celle que l'on utilise toujours de nos jours sous le nom de définition tarskienne de la vérité à la base de la sémantique tarskienne (utilisée en théorie des modèles). Ensuite, si l'on combine le théorème de Gödel auquel Perthmâd fait allusion (le théorème d'incomplétude) à une autre théorème fondamentale de Gödel (son théorème de complétude : une théorie est cohérente si et seulement si elle a un modèle), on aboutit à la conclusion du texte kantien cité ci-dessus. Une théorie (disons ZF, la théorie axiomatique des ensembles) qui fournirait un critère matérielle de sa vérité serait en mesure d'engendrer son propre contenu (fournirait un modèle d'elle-même), serait donc cohérente (en vertu du théorème de complétude) ce qui contredirait le théorème d'incomplétude.
Le théorème d'incomplétude clos une période historique au cours de laquelle la thèse centrale de la Critique de la Raison Pure fut attaqué de toute part par des logiciens, et Gödel finit par donner raison à Kant. :-)
On gagne déjà beaucoup à pouvoir faire tenir une foule de recherche sous la formule d'un seul problème. Par là, en effet, on ne facilite pas seulement pour soi-même son propre travail, en se le déterminant avec précision, mais on rend aussi plus facile à quiconque veut l'examiner de juger si nous avons ou non satisfait à notre dessein. Le problème propre de la raison pur est donc contenu dans la question suivante : Comment des jugements synthétiques a priori sont-ils possibles ? […]
Dans la solution du problème précèdent est engagée en même temps la possibilité du pur usage de la raison pour fonder est développer toutes les sciences qui contiennent une connaissance théorique a priori des objets, c'est-à-dire la réponse à ces questions :
Comment la mathématique pure est-elle possible ?
Comment la physique pure est-elle possible ?
Kant, ibid.
À cette subdivision de la question, précède le texte suivant :
Les jugements mathématiques sont tous synthétiques. Cette proposition semble avoir échappé jusqu'ici aux observations des analystes de la raison humaine, et même être exactement opposée à toutes leurs conjectures, bien qu'elle soit incontestablement certaine et très importantes dans ses conséquences. En effet, comme on trouvait que tous les raisonnements mathématiques procédaient tous d'après le principe de contradiction (ce qu'exige la nature de toute certitude apodictique) on se persuada que les principes étaient connu aussi étaient connus à partir du principe de contradiction : en quoi ces analystes; car une proposition synthétique peut bien être saisie d'après le principe de contradiction, mais seulement de telle sorte qu'une autre proposition synthétique soit supposée, d'où elle puisse être déduite, mais jamais en elle-même.
Kant, ibid.
Ce qu'a prouvé Gödel, c'est que la logique formelle (et donc le principe de contradiction) ne peut légitimer à elle seule le raisonnement par récurrence : le principe du raisonnement par récurrence est un pur jugement synthétique a priori.
Il y a un membre de linuxfr qui a pour signature quelque chose du style : «BeOS le faisait déjà il y a vingt ans ». Pour ma part, d'une manière générale, je dirais : ce que font les théories des types contemporaines, Kant le faisait déjà il y a plus de 200 ans. Par exemple, la logique de Hoare utilisée par frama-c, c'est dans la Critique de la Raison Pure; ou bien la programmation par contrat, la gestion de propriété des espaces mémoires par Rust ou Mezzo, c'est dans la Doctrine du Droit (que l'on peut voir comme une théorie de typage du droit romain). :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Petit ajout que j'ai oublier de préciser avec le type contradictoire.
typecontradiction={faux:'a.'a;}leti={faux=Obj.magic1};;vali:contradiction={faux=<poly>}(* là c'est bon *)1+i.faux;;-:int=2(* là ça segfault !! *)1.5+.i.faux;;
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Juste concernant Go, il me semble que l'approche (en tout cas des critiques que j'ai pu lire ici et là) n'est pas type-safe dans le sens où interface{} serait en réalité le type top comme la classe Object en Java - ce qui permet de facilement bypasser le système de type de Go.
C'est type-safe le interface{}, c'est un type existentiel. Par contre tu perds la garantie du typage statique et tu dois faire des assertions de type ou du switch sur type : il faut faire du typage dynamique. C'est comme en Python, en somme, sauf qu'en dehors de interface{} on a bien la garantie d'un typage statique (sans quantification universelle sur les types, c'est-à-dire, sans généricité mais c'est déjà pas trop mal). En gros, je le vois comme ça (je me trompe peut être) :
typeintf=E:'a->intfleti=E1
mais comme Go garde des informations de typages au runtime, on peut retrouver à l'éxecution la valeur contenue dedans avec son type : pour Go, i est de type int et vaut 1.
variinterface{}i=1fmt.Printf("i est de type %T et vaut %v",i,i)// affiche : i est de type int et vaut 1
Ce qui n'est pas type-safe, c'est une valeur de tout type (avec quantification universelle sur les types). On parle de l'aspect unsound du système de type de Java (qui a des génériques) ou de la valeur undefined de Haskell ?
Là, on contourne clairement le système de types, mais on annonce la couleur en utilisant le module Obj. ;-) Le type de faux, c'est le principe ex falso quodlibet.
Par contre j'ai un peu trop surestimé le système des interfaces : j'ai cru que c'était du type classes à la Haskell mais sans types paramétriques. En fait non, c'est clairement moins bien fait, tu ne peux pas avoir d'interface pour de telles méthodes :
On ne peut pas définir le type interface de ceux qui implémentent la méthode Add : c'est nul et ça pourrait limiter le besoin de recourir à interface{}. Déjà qu'il n'ont pas de génériques (types paramétriques), ils auraient pu faire un effort de ce côté là.
Le mécanisme des arguments implicites (s'il était implémenté) permettrait d'inférer automatiquement le 'a add à utiliser en fonction du type 'a des autres paramètres passés à add par unification, là où pour l'instant on doit le passer explicitement (c'est ce que font les types classes de Haskell mais en plus général, les types pouvant être paramétriques comme avec les monades). Go fait cela mais de manière très restreinte : la variable de type 't ne doit pas apparaître dans le type des champs de l'enregistrement. /o\
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Tu devrais tout de même jeter un œil à la vidéo de Xavier Leroy dont j'ai donné le lien au-dessus, il y parle pendant une vingtaine de minutes du milieu de l'avionique et de ses exigences de certification.
C'est sûr, ce n'est pas comme si je n'avais pas déjà certifié 2 ou 3 logiciels.
Je sais bien que tu n'ignores pas les exigences en question, mon conseil de visionnage était là pour te dire que Xavier Leroy non plus, que son projet s'inscrit dans cette démarche d'exigence (raison pour laquelle il aborde le secteur de l'aéronautique), et que tu pourras peut être comprendre en quoi ce logiciel est une avancée dans la recherche de sécurité par rapport aux méthodes antérieures — celles que tu connais déjà, justement.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Je crois bien que le ton de nos échanges est monté par ma faute, j'en suis désolé. J'étais mal luné l'autre jour, j'aurais du tourner mes doigts dix fois avant d'écrire, j'en suis désolé. :-/
Le bug peut être également dans le model.
Tout à fait, mais cette problématique est hors de portée de la logique et des approches formelles.
Cette partie de la logique de notre connaissance peut donc être nommée analytique, et elle est la pierre de touche, du moins négative, de la vérité, puisqu'il faut d'abord contrôler et estimer d'après ces règles toute connaissance selon sa forme, avant de l'examiner selon le contenu pour établir si, à l'égard de l'objet, elle contient une vérité positive. Mais, comme la simple forme connaissance, aussi d'accord qu'elle puisse être avec les lois logiques, ne suffit (nullement) pour établir la vérité matérielle (objective) de la connaissance, personne ne peut se hasarder de juger des objets avec la simple logique, et à en affirmer quelque chose, sans en avoir entrepris auparavant une étude approfondie en dehors de la logique, pour ensuite essayer simplement de les utiliser et de les lier en un tout cohérent selon les lois logiques, mieux encore, des les examiner simplement d'après elle. Cependant, il y a quelques choses de séduisant dans la possession d'un art aussi spécieux, celui de donner à toute nos connaissances la forme de l'entendement, quelque vide et pauvre qu'on puisse être à l'égard de leur contenu, que l'on use de cette logique générale, qui est simplement un canon pour l'évaluation, comme d'un organon pour produire réellement, du moins en en donnant l'illusion, des affirmations objectives, ce qui est en fait abuser de cette logique.
Kant, Critique de la Raison Pure.
La partie graissée correspond à ce que tu dis : si l'erreur est dans le modèle (le contenu, la matière), la logique qui ne s'occupe que de la forme ne peut rien y faire. Pour grossir le trait, la logique n'a rien à reprocher au raisonnement suivant :
les hommes sont immortels
or je suis un homme
donc je suis un immortel
celui qui se croirait immortel, en se justifiant du fait que la logique ne trouve rien à redire à ce syllogisme, ferait rire n'importe qui face à lui. :-D
Pour faire une analogie avec le domaine juridique : la logique s'occupe des vices de forme dans la procédure. En l'absence de vice de forme, il faut tout de même un procès pour débattre de l'issue du cas : on y examine la question de droit (la majeure du raisonnement : les hommes sont immortels) et la question de fait (la mineure du raisonnement : je suis un homme). Ici, la majeure est en tort : l'accusé est innocenté, déclaré non coupable, ou plutôt non immortel. La question de fait en revanche ne fait ici pas de doute; en cas de non lieu c'est celle-ci qui n'a pu être justifiée.
J'imagine que pour vérifier le comportement du C par rapport aux instructions assembleur, il faut modéliser ses instructions, ce qui n'est pas forcément simple.
Tout à fait : c'est bien pour cela que je parlais d'un travail de titan ! Il faut formaliser les instructions assembleurs (de trois architectures qui plus est : PowerPc, ARM et x86), formaliser la sémantique d'un sous-ensemble assez large du C, puis prouver que toutes les transformations-traductions du code préservent les sémantiques. Mais Xavier Leroy et son équipe on pu réaliser cet exploit (car s'en est un, une première au monde pour un compilateur) parce qu'ils avaient déjà un forte expérience dans l'écriture de compilateur et de sémantique des langages de programmation : ils en avaient entrepris auparavant une étude approfondie en dehors de la logique. ;-)
J'adore ta condescendance, tu n'a aucune idée de comment le problème est géré actuellement dans de vrai projet, mais tu la ramènes quand même.
Nulle condescendance dans mon message, je mets cette réaction sur le dos du ton que prenaient nos échanges. Je ne suis pas sans savoir comment cette question est gérée en l'absence d'un tel outil, mais je tiens à signaler que la garantie que CompCert apporte sera à jamais inaccessible à ces méthodes. Raison pour laquelle Gérard Berry, qui n'ignore pas non plus ces méthodes, a écrit :
Il s’est agi de réaliser un compilateur du langage C qui soit non plus certifié seulement pour la qualité des méthodes de développement et de test comme dans la norme DO-178C, mais bel et bien prouvé mathématiquement correct et donc vraiment garanti sans bugs.
Le graissage est de moi pour bien souligner que les méthodes auxquelles tu fais allusion, si elle sont acceptées en pratique, ne pourront jamais apporter ce niveau de garanti (j'espère que tu m'épargneras un débat épistémologique sur la distinction entre la connaissance rationnelle et la connaissance expérimentale afin de justifier cette position).
Je tiens à préciser à nouveau que ce compilateur fait partie de la chaîne d'outils que AbsInt vend à ses clients dont Airbus. :
Check your C code for runtime errors with Astrée.
Compile the code using CompCert
Check your stack usage with StackAnalyzer
Analyze the execution time with aiT
Tu n'as compris que la forme était le plus important pour travailler avec un tel outil, pour la compréhension même de ce qu'ils font d'un point de vue métier.
Bien sûr que j'ai le compris : un tel outil doit savoir cacher ses entrailles pour exposer à l'utilisateur ses concepts métiers pour qu'il se focalise sur ce qu'il connaît. Il n'empêche que sous le capot, c'est de la traduction mathématique et de la preuve mathématique, quand bien même l'utilisateur n'en a pas conscience. Un bon outil est celui qui sait se faire discret sur son fonctionnement : celui qui l'utilise, celui qui le construit et celui qui le répare sont rarement les mêmes personnes, n'ont pas les même savoir, ni les mêmes compétences.
D'ailleurs pour illustrer la chose : je ne connaissais pas Go, si ce n'est de nom. Résultat je suis allé jeter un coup d'œil, et bien je trouve leurs choix tout sauf bêtes contrairement à ce que certains ont pu dire. Il n'y a certes pas de généricité (sauf sur quelques types comme les tuples ou les tableaux) mais leur système de type interface est très ingénieux et semble compenser allègrement à l'usage l'absence de généricité. D'un point de vue formel, au premier abord (je n'ai pas creusé plus que cela) ça s'apparente grandement à des fonctions avec arguments implicites sur du lambda-calcul simplement typé avec enregistrements (un langage avec des fonctions comme citoyen de première classe pour lequel un argument de certaines fonctions est inférer par le compilateur)1. Le polymorphisme au lieu d'être paramétrique (comme C++, Java, Haskell…) et ad-hoc mais vérifier à la compilation. Choix qui offre aux développeurs un large panel de technique de programmation sans l'assomer avec des abstractions difficiles à comprendre, donc à maîtriser et donc à utiliser (comme le sont les modules ou les GADT pour toi).
Haskell a cela avec ses type classes, mais OCaml manque d'un tel dispositif ce qui rend un code qui fait un usage intensif de modules très vite incompréhensible pour celui qui n'en est pas l'auteur. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Les classes de type marchent assez bien pour gérer le type Dyntype a, parce que c'est typiquement le genre de valeurs que tu veux passer implicitement, et pour lequel tu n'as pas envie/besoin d'avoir plusieurs implémentations pour un même type.
On en revient toujours au fait que les modules implicites seraient une fonctionnalité géniales pour OCaml. Elle rendrait les modules encore moins citoyen de seconde classe que ne le font les first-class modules. ;-)
Lorsque j'avais mentionné à Leo White l'article-tutoriel sur les structures canoniques en Coq, il m'a répondu l'avoir déjà lu (effectivement, cela fait même partie des références de l'article de présentation du prototype sur les modules implicites). Cela étant, ils mentionnent un autre article intéressant, qui pourrait servir de base pour la formalisation, dans leurs références : The Implicit Calculus: A New Foundation for Generic Programming qui mentionne aussi le tutoriel sur les structures canoniques. Mais il me vient à l'esprit une interrogation :
l'article sur le calcul implicite se limite au système F ;
les auteurs précisent que les structures canoniques n'ont pas été formellement spécifiées ;
le mécanisme des arguments implicites est décrit pour tous les système du lamda-cube dans la partie 4 de la thèse de Amokrane Saïbi (en français \o/).
S'il est vrai que dans sa thèse il décrit un algorithme d'unification plutôt qu'une formalisation à base de règles d'inférence à la Gentzen, les deux approches ne me semblent pas si éloignées et je ne vois pas ce qu'il manque à ce système pour fournir ce dont ont besoin les modules implicites pour synthétiser les arguments implicites.
Dans un autre registre, sur le statut des modules dans le langage : que penses-tu des travaux de Rossberg, Russo et Dreyer sur 1ML présentés à l'ICFP en 2015 ? Cela demanderait trop de modifications à apporter au langage pour avoir cela dans OCaml ?
An alternative view is that 1ML is a user-friendly surface syntax for System Fω that allows combining term and type abstraction in a more compositional manner than the bare calculus.
et ça résoudrait les incompréhensions de Nicolas Boulay, ils y définissent les modules avec la syntaxe des enregistrements. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
compcert a été prouvé avec seulement ce bout de code ? Sans rien de manuel ?
Bien sur que non, c'est un travail de titan le code complet ! C'était pour illustrer ma proposition « la quantité d'erreurs attrapées à la compilation dépend de l'expressivité du système de types », en montrant un système de types tel que son expressivité dispense d'avoir à recourir à des tests unitaires. Ce théorème, qui n'est qu'une infime partie du code du compilateur, est celui que Xavier Leroy utilise dans sa vidéo comme illustration : c'est normal, c'est lui qui exprime que son compilateur est optimisant est n'apporte aucune modification de comportement à la compilation (si il y a un problème dans le code compilé, il se trouve déjà dans le code C).
Pour info, j'ai bossé 10 ans dans l'aéronautique, et l'usage des compilos C certifié c'était plutôt : "il faudrait prendre le temps de voir ce que cela donne".
Je le sais bien, c'est pour cela que j'ai parlé de cette industrie. Au sujet du projet CompCert C, Gérard Berry (lui, tu le connais il a cofondé l'entrepise qui fut (est ?) ton employeur et est le père du langage Esterel) l'a décrit dans le bulletin de la société informatique de France ainsi :
CompCert, l’autre grande contribution de Xavier Leroy et de son équipe, est une aventure encore unique sur le plan mondial. Il s’est agi de réaliser un compilateur du langage C qui soit non plus certifié seulement pour la qualité des méthodes de développement et de test comme dans la norme DO-178C, mais bel et bien prouvé mathématiquement correct et donc vraiment garanti sans bugs.
Pour info le compilateur est un produit (il n'est pas libre, seulement pour un usage non-commercial) de l'entreprise AbstInt :
Certification and qualification
Current safety standards such as ISO 26262, DO-178B/C, IEC-61508, EN-50125 and others require identifying potential functional and non-functional hazards and demonstrating that the software does not violate the relevant safety goals.
Abstract-interpretation based tools such as aiT, StackAnalyzer, and Astrée provide formal verification with 100% complete and reliable results. They are therefore perfectly suited to be used for certification.
The qualification process is greatly simplified by our Qualification Support Kits. Additionally, Qualification Software Life Cycle Data Reports provide details about our development processes.
qui a pour client Airbus et pour partenaire Esterel Technologies. ;-) Pour Airbus, ils utilisent leurs analyseurs statiques de code (aiT analyse le comportement temporel, StackAnalyzer l'absence de stack overflow et Astrée l'absence de runtime error) :
For many years Airbus France has been using aiT, StackAnalyzer and Astrée in the development of safety-critical avionics software for several airplane types, including the A380, the world’s largest passenger aircraft. The analyzers are used as part of certification strategy to demonstrate compliance to DO-178B, up to Level A.
et Compert C s'incrit dans la chaîne des outils : si le code C est propre et garanti c'est bien, mais si le compilateur introduit un bug c'est un peu couillon, tu ne crois pas ?
Je crois que je peux te répondre la même chose, mais pas pour le même domaine.
T'es sûr ? Tu faisais (ou fais) quoi comme travail chez Esterel ? Tu y appris quoi chez eux pour avoir écrit cela ?
Les exemples de preuve sont très matheux. Cela ne ressemble pas à des preuves "industrielles" (à base de bout de spec, de bout d'exemple, de ne "plante jamais", a un temps d'exécution borné).
T'as pas compris depuis le temps que ce tu qualifies de "industrielles", ce sont aussi des preuves de matheux ? ;-)
Tu devrais tout de même jeter un œil à la vidéo de Xavier Leroy dont j'ai donné le lien au-dessus, il y parle pendant une vingtaine de minutes du milieu de l'avionique et de ses exigences de certification.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le plus malin est en général le premier qui cède
Posté par kantien . En réponse à la dépêche Seconde mise en demeure pour l'association LinuxFr. Évalué à 10.
Ce qu'ils ont fait lors de sa promotion en dépêche.
Si le journal était purement factuel et reprenait la forme et le contenu de mes deux sources1 :
La dépêche (dont je suis également l'auteur) est autrement plus fouillée et détaillée, tandis que le journal s'apparente plus à une dépêche AFP.
Ce qui repose l'éternel débat sur le choix terminologique de linuxfr entre dépêche et journal. :-P
on notera que l'article de M. Gallaire n'en fait pas partie. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2. Dernière modification le 08 novembre 2017 à 12:31.
C'était une formation en logique mathématique et sur les fondements de l'informatique. Personnellement, à l'époque, la partie fondements de l'informatique ne m'intéressait pas spécialement. Je voulais surtout approfondir mes connaissances en logique et voir ce qu'avaient donné les attaques contre la philosophie kantienne des mathématiques (j'ai lu la Critique de la Raison Pure à la fin de ma spé, et je suis kantien depuis cette époque). Pour ceux intéressés par l'informatique, d'après la brochure sur les débouchés, il semblerait qu'ils finissent par faire une thèse et de la recherche (dans les organismes publiques ou en R&D chez des industriels genre EDF).
J'ai bien conscience qu'une telle formation est à part par rapport aux formations courantes des ingénieurs informaticiens.
Démontrer comment, par l'exemple ? Mais, de mon point de vue, un fait ne prouve pas grand chose : je m'intéresse surtout aux méthodes et à leur limite. Je suis un obsédé de la certitude : qu'est-ce que la certitude ? de quoi peut-on être certain ? quelles méthodes peuvent espérer atteindre à la certitude, lesquelles ne le peuvent pas ? font partie des questions qui m'obsèdent. Et de ce point de vue, l'induction et la méthode expérimentale reviennent à cela :
ou pour citer Einstein résumant la philosophie sceptique de Hume : « l'empirique, dans la connaissance, n'est jamais certain (Hume) ». Il ne fut néanmoins pas convaincu par la réponse kantienne aux objections de Hume : « Kant propose alors une pensée. Sous la forme présentée elle est indéfendable mais elle marque un progrès nette pour résoudre le dilemme de Hume ». Pour ma part, je la trouve on ne plus défendable, et la méthode qu'il employa est analogue à celle utilisée par tous les systèmes de types des langages de programmations. Pour pousser le distinguo à l'extrême : je n'ai aucune certitude que le soleil se couchera se soir, mais je n'ai aucun doute quant à ce qu'exprime le théorème de Pythagore.
Pour revenir aux outils d'analyses et de sécurisation de code, il ne s'agit pas nécessairement de spécifier dans les moindres détails chaque bout de code et d'apporter la preuve du respect de la spécification, mais il est peut être envisageable d'ajouter certaines annotations en commentaires (à la manière de frama-c) pour avoir un système de type à l'expressivité plus riche que celui du C. Le système de type de C, de fait, exprime des spécifications sur le code mais, comme c'est peu ou prou la logique propositionnelle du premier ordre, on ne peut pas y exprimer grand chose : ce que fait le code et comment l'utiliser est beaucoup trop sous-spécifié avec un tel système de type.
Prenons un exemple. Je ne connaissais Coccinelle que de nom, je suis allé voir un peu leur site, et sur la page consacrée aux évolutions collatérales ils donnent deux exemple : ajout d'un argument à une fonction et changement dans le protocole d'initialisation des pilotes. Il semblerait que les pilotes aient mis un certain temps à s'adapter correctement à ce changement d'interface dans le cœur du noyau. Ces changements il faut bien les documenter quelque part ? Pourquoi pas dans une langue proche par sa syntaxe et son vocabulaire de l'anglais, mais à la grammaire plus régulière, et l'écrire en commentaire du code modifié ? On pourrait alors avoir une logiciel d'aide à l'audit qui détecterait automatiquement les mauvais usages des nouveaux codes.
Entre un audit totalement manuel et un audit partiellement automatisé, dans le monde de l'informatique ça doit pouvoir convaincre (pourquoi faire à la main ce qu'une machine peut faire pour moi ?). Je ne suis membre d'aucune des deux communautés (celle du noyau et celle de la recherche), mais je sais que la seconde est en état de fournir ce genre d'outil à la première. Néanmoins, pour cela, il faudrait une coopération et une synergie entre elles qui ne semblent pas exister aux dires de gasche. Je ne peux que trouver cela dommage.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Comportement attendu
Posté par kantien . En réponse au journal Compilateur trop intelligent. Évalué à 2.
C'est sur ce point que je ne sais pas ce qui est permis par le standard du C. Il y a des exemples de undefined behavior dans le manuel mais pas celle de l'exemple du journal : les exemples sont les overflow sur l'arithmétique signée (qui sont définies dans CompCert par les règles de l'arithmétique modulaire) et les accès hors bornes pour les tableaux qui renvoient une erreur.
D'après le deuxième principe que je cite du manuel « Second, the compiler is allowed to select one of the possible behaviors of the source program », le compilateur peut choisir n'importe quel comportement possible en accord avec la norme en cas de non déterminisme; c'est sur ce point que je n'ai pas bien compris si le choix de clang est acceptable (certains disent que oui, d'autres disent non) et pour moi cela reste encore bien obscur.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Je suis étonné du caractère si récent de la prise en compte d'une telle problématique. J'ai terminé mes études il y a une quinzaine d'années et ce genre de questions étaient au cœur de la formation. Personnellement, l'utilité pour l'informatique était une chose qui, à l'époque, me semblait un cas d'application amusant mais sans plus; je regardais la chose d'un air amusé, les fondements des mathématiques m'important plus que ceux de l'informatique. Ce n'est que très récemment que je me suis repenché sur le lien avec le développement logiciel. À l'époque, les deux seuls langages que l'ont m'a enseigné était OCaml et Coq : avec le premier je m'étais amusé à faire un système de calcul formel sur l'arithmétique transfinie de Cantor, et avec le second j'avais formalisé quelques résultats élémentaires d'arithmétiques. Autant dire des questions de peut d'intérêt pour du développement logiciel.
Ceci étant dit, il est connu de longue date que la qualité logicielle relève de la preuve mathématique. Les approches dignes des sciences expérimentales à coup de tests unitaires ou de fuzzer, c'est gentil : ça peut détecter la présence de bugs, mais cela n'en prouvera jamais l'absence. À un moment, quand on affirme, il faut pouvoir prouver, quitte à le faire à la main :
pourrait être la devise des kantiens.
Quand je lis, par exemple, dans ce fil, que Nicolas Boulay demande qu'il faut démontrer la supériorité d'une solution avant de la mettre en œuvre et que gasche doit lui répondre :
je tombe des nues. :-O Mais enfin, c'est une évidence pour qui est un minimum rigoureux intellectuellement ! On pourrait y rajouter en écho ce passage de l'évangile selon Saint Luc (chapitre 6, versets 47-49) :
ou encore cet extrait de la préface des Prolégomènes à toute métaphysique future qui pourra se présenter comme science de Kant :
Lorsque gasche affirme que c'est un investissement sur le long terme :
cela va également de soi. Mais plus le projet tarde à s'y mettre, plus la base de code (déjà très volumineuse) augmentera et plus il sera difficile, voire surhumain, de mettre en pratique ce genre d'approche de contrôle qualité. Il vient donc naturellement à l'esprit cette question : la communauté en charge du développement du noyau est-elle sensible à ces questions ou s'en moque-t-elle fondamentalement ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 5.
Là, il y à un truc que je ne comprends pas du tout. Je n'avais pas prêté attention au message de ta part auquel gasche t'a répondu en présentant ce DSL, mais tu y reprochais à OCaml de ne pas générer des instructions SIMD en écrivant :
Il te répond avec un langage qui fait cela pour du code sur GPU, et tu réponds que ça ne te parle pas ? C'est quoi le problème ? Qu'ils utilisent la lettre
pour définir des fonctions ? Qu'ils écrivent
reduceet nonfold?Si j'écris cela :
alors tu comprends, mais tu voudrais que cela génère du code optimisé avec instructions SIMD ?
Mais quand on écrit :
alors tu ne comprends plus ?
On pourrait rendre le code python encore plus concis avec :
mais quand on sait ce qu'est un
fold(oureduce), unmapet une composition de fonctions, l'équivalence des deux écritures est évidente.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Comportement attendu
Posté par kantien . En réponse au journal Compilateur trop intelligent. Évalué à 4. Dernière modification le 04 novembre 2017 à 08:46.
Tu n'es pas très joueur ! Moi, quand je m'ennuie, je joue à la roulette russe; ou en plus fun, je fais comme cap'tain sports extrêmes : je fais du saut à l'élastique mais sans élastique, avec un élastique on a aucune sensas' ! :-P
Pour prendre le manuel d'un compilateur qui ne s'amuse pas à changer la sémantique du code (« Traduttore, traditore » ou « Traducteur, traître » dit son manuel) :
et à la question « qu'est-ce qu'un comportement observable ? », il précise :
Je ne connais pas bien la sémantique du C mais, pour l'exemple du journal, il me semble bien que l'optimisation de clang ne respecte pas ces principes.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Corrigé
Posté par kantien . En réponse à l’entrée du suivi Problème de parsing sur les formules latex. Évalué à 3 (+0/-0).
Merci ! :-)
Je teste :
Ceci est à mettre en parallèle avec les énoncés que l'on ferait sur l'encodage des entiers naturels dans ZF, où on écrirait
pour énoncer une propriété des entiers. Ici le quantificateur universel sur 
correspond à une vérification dynamique de type avant de continuer « l'exécution » vers le conséquent.
xparcourt la collection de tous les ensembles (intreface{}) puis l'énoncé est une proposition hypothétique dont l'antécédentEt ça marche !! :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Mieux ?
Posté par kantien . En réponse à l’entrée du suivi Impossible de répondre à un commentaire. Évalué à 2 (+0/-0).
Au passage, je me demande s'il n'y a pas un lien avec une autre entrée de suivie que j'avais faite. Quand on met plusieurs formules en lignes et que l'on mélange avec du texte en chasse-fixe, elles ne sont pas toutes traitées.
Un test : le
(d'où le 
.
\de Haskell ou Elm) du lambda-calcul était à l'origine en majusculeJe veux bien essayer de voir d'où cela vient et tenter de corriger le problème, mais je ne sais pas par où commencer dans la base de code du site.
P.S : après prévisualisation, le test semble bien traiter le
, mais ce n'est pas toujours le cas. Dans ce commentaire, j'ai un 
.
$x \in \omega$non interprété enSapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Mieux ?
Posté par kantien . En réponse à l’entrée du suivi Impossible de répondre à un commentaire. Évalué à 3 (+0/-0).
C'est bon, ça marche. Merci ! :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
La correspondance s'étend aussi au raisonnement par l'absurde et donc à la logique classique, ce sont les exceptions dans les langages de programmation (les blocs
try-with-finally). Voir ce texte de Jean-Louis Krivine (page 3).Ce n'est qu'une question de vocabulaire : il y a d'un côté les jugements que l'on considère (calcul des prédicats ou calcul propositionnel, au premier ou second ordre) et de l'autre les règles de déductions (classique ou intuitionniste). Comme dans une logique on considère à la fois les règles de formations des jugements et les règles de déduction, pour éviter toute ambiguïté, il serait sans doute préférable de parler de logique classique du premier ordre et de logique intuitionniste du premier ordre.
Le quantificateur universel c'est le
du lambda-calcul, le
\de Haskell, lefunde OCaml… c'est lui qui abstrait sur la totalité d'un domaine et, effectivement, dans le calcul des prédicats, on abstrait sur tout le domaine du modèle — sur tout l'univers des ensembles dans ZF. Les langages dynamiques sont des langages avec typage statique… qui n'ont qu'un seul type statique. Là où dans les théories des types, comme en Coq, on peut n'abstraire que sur les valeurs d'un type donné.L'implication est bien toujours le signe d'une fonction mais, dans mon exemple, elle ne spécifie rien sur sa sortie pour une entrée qui n'est pas un ordinal. Si on reprend mon énoncé (légèrement modifié) :
il dit qu'à tout ensemble
x, il peut en associer un autrey. Lorsquexest un ordinal, l'énoncé affirme queyest son prédécesseur qui est aussi un ordinal, mais dans le cas contraire (qui peut arriver, on a quantifié sur tous les ensembles), il ne dit rien sury. La preuve d'un tel théorème expose, dans le cas oùxest un ordinal, un moyen de produire un telyet fournit la preuve queyest aussi un ordinal. En revanche, dans le cas oùxn'est pas un ordinal, elle ne dit rien sury(si ce n'est que c'est un ensemble, donc n'importe quelle valeur possible). Ce qui me fait penser à ce code Go :Il prend en entrée toute valeur possible (n'importe quel ensemble pour ZF), dans le cas où c'est un
uintrenvoie unyselon la même spécification que l'énoncé, ou bien renvoie une erreur si l'entrée n'est pas de typeuint(cas de la preuve qui ne dit rien sury, on renvoie une erreur). Ici le procédé est totalement constructif au sens des règles de déductions intuitionnistes. Le fait que la preuve du théorème prouve aussi queyest un ordinal, quandxl'est, se retrouve sur le type de sortie de la fonction en Go.Après réflexion, on pourrait faire quelque chose de similaire en OCaml. Pour cela, il faut un type dans lequel on puisse plonger des valeurs de n'importe quel type : on parle de type universel. La signature d'un module fournissant un tel type est :
Je passe les détails d'implémentations d'un tel module (il faut utiliser un type somme extensible, comme l'est celui des exceptions dans le langage) et montre juste son usage en supposant que l'on a
module U : Univ, c'est à dire un module fournissant un tel type :Pour en revenir aux différentes logiques, le problème est bien dans le calcul des prédicats. Il est tel que, lorsqu'on l'interprète, toute les choses dont il parle sont considérées comme étant homogènes. Par exemple, si on veut formaliser la théorie des espaces vectoriels dans un tel symbolisme, il faut mettre les scalaires et les vecteurs dans un même sac fourre-tout et un modèle d'une telle théorie devra donner une signification à la somme d'un scalaire et d'un vecteur (ce qui, fondamentalement, n'a aucun sens dans un tel cadre). Raison pour laquelle je disais que les approches de la logique via la théorie des types captent bien mieux la notion de concept : le concept de scalaire ne sera nullement mélangé arbitrairement avec celui de vecteur, ce seront deux types distincts.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3. Dernière modification le 02 novembre 2017 à 15:07.
Moi aussi, je n'avais jamais entendu parler de lambda-calcul avant mon DEA. Ce que je voulais dire, dans le fond, c'est que le niveau d'abstraction requis pour le comprendre relève du premier cycle en mathématique (une fois que l'on a expliqué ce que signifie le lambda, ce qui prend deux minutes). Tu trouves (si je me fie à ce que j'ai déjà lu) que elm est un bon langage pour faire du développement web : ce type de code doit être assez standard en elm. Elm a la même syntaxe que Haskell où le lambda est remplacé par l'anti-slash
\, c'est tout. Après c'est du map-reduce, on ne peut plus classique en programmation fonctionnel, ce qui n'exige pas un niveau de compréhension d'un niveau doctoral.En OCaml, on l'écrirait ainsi :
L'avantage pour des chercheurs de passer par du lambda-calcul, sans ajouter trop de sucre syntaxique, est d'avoir rapidement un prototype opérationnel comme preuve de concept.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Tu ne penses pas que tu exagères un peu là ? C'est du niveau premier cycle en mathématique (allez, fin de premier cycle pour être gentil).
Exemple sur la définition du produit scalaire :
et sa traduction en python :
la fonction
zipexiste aussi en python :la différence étant que les fonctions
mapn'ont pas la même interface entre les deux langages. La définition du produit scalaire entre vecteurs en python, je l'ai prise de la documentation python officielle. Sinon, voir aussi cette réponse sur stackoverflow :C'est du python on ne peut plus idiomatique.
Et ne me parle pas de je ne sais quel grade doctoral : j'ai le même grade universitaire qu'un ingénieur, à savoir un bac+5.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2. Dernière modification le 31 octobre 2017 à 10:58.
Je précise ici ma réponse sur ZF vu comme un langage dynamiquement typé. On pourra continuer la discussion de cette sous-question sous ce commentaire et laisser celle sur la physique à un autre fil.
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. J'ai déjà écrit ailleurs un commentaire, en réponse à une question de Michaël, sur la différence entre les deux notions, le rapport entre programmes et preuves de théorème (correspondance de Curry-Howard) et la distinction entre les systèmes de types de OCaml et de Coq.
Si ça pose problème : dans un cas l'énoncé est prouvable dans ZF (c'est un théorème) dans l'autre il est réfutable, et cela selon les règles intuitionnistes (sans raisonnement par l'absurde). Exemples :
Le premier se paraphrase en français ainsi : tout ordinal fini est soit vide, soit le successeur d'un ordinal fini. Le second se paraphrase ainsi : tout ensemble est soit vide, soit le successeur d'un autre. Tu remarqueras, au passage, que le français est tout à fait apte à exprimer de tels énoncés, sans recourir à un symbolisme quelconque. ;-)
Le premier est trivialement vrai, le second est trivialement faux dans ZF. Le premier exprime le type de la fonction prédécesseur. En OCaml, on écrirait cela ainsi :
En Coq, cela se formalise de manière assez similaire :
Ici la fonction
predest sous-spécifiée (elle a pour typeNat -> Nat), mais on pourrait lui donner un type plus précis analogue à ce qu'exprime le théorème, qui est la traduction en Coq du premier énoncé pour ZF. En revanche les contraintes de typage statique de l'un ou l'autre langage ne permettent pas d'exprimer le second énoncé. Contrairement à Python :La fonction
predavec vérification dynamique de type s'apparente au premier énoncé, tandis que la seconde fonctionpred_unsafes'apparente au second.J'espère que la chose te semble plus claire maintenant. Il vaudrait mieux, du moins, car c'est une promenade de santé par rapport au problème du rapport entre le kantisme et ce qu'il entend par réalité. Ma réponse à ce sujet viendra plus tard, peut être ce midi ou en fin de journée si je trouve le temps qu'il faut pour la rédiger.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
Les kantiens n'ont jamais nié une telle chose.
Bah, quand on me dit que la pierre a une existence propre spatio-temporellement déterminée, j'interprète cela comme abstraction faite de tout rapport à un observateur possible, c'est-à-dire que l'on se débarrasse de l'observateur. Autrement dit, qu'il y est ou non des hommes, il existe un monde dans lequel des pierres évoluent dans l'espace et le temps et la physique est là pour découvrir les lois d'un tel monde. Ce que disent les kantiens, ce n'est rien d'autre que ce que disait Socrate : nous ne voyons que des ombres sur un mur, tels les esclaves de l'allégorie de la caverne. Qu'il y est quelque chose qui nous apparaisse comme une pierre spatio-temporellement déterminée, que cette chose soit bien réelle, nous l'accordons; nous disons juste qu'elle n'est telle que pour les êtres humains.
Je te répondrai plus en détail demain, mais j'ai l'impression que tu te méprends (comme Einstein lui-même d'ailleurs) sur ce que veulent dire les kantiens quand ils affirment que la pierre (ou tout autre objet physique) ne sont pas des choses en soi existant « sans nous ».
Disons que sans écrire un énoncé à quantificateur universelle borné (la condition
), on risque la contradiction ou l'énoncé vide de sens. ;-)
Un peu mon neveux ! La logique s'occupe des règles pour former des concepts, des règles pour former des jugements à partir de ces concepts et des règles pour enchaîner ces jugements entre eux ou raisonnements. Le plan de la doctrine générale des éléments du traité sur la logique de Kant :
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2. Dernière modification le 30 octobre 2017 à 12:21.
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).
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. Deuxièmement, 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; et 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 pourrais développer ce point en faisant une analyse comparée d'un texte d'Enstein (un article qu'il a écrit sur Bertand Russel) et de la plaidoirie de Kant pour se défendre d'être un idéaliste (au sens que ce terme à en philosophie), si tu souhaites plus de précisions. La plaidoirie de Kant est, dans le fond, une réponse à l'objection que tu m'opposes.
Ton interprétation (libre) ne tombe pas loin de la réalité : telle était l'intention primordiale de la théorie, mais c'est « mal » fait. L'idée étant de voir un ensemble comme un concept dont l'extension (la totalité de ses éléments) dénote les objets tombant sous le concept (d'où, par exemple, l'axiome d'extensionnalité affirmant que deux ensembles ayant les mêmes éléments sont égaux), et l'inclusion entre ensembles exprimant alors la subordination entre concepts, c'est-à-dire du sous-typage.
Ma comparaison avec le typage dynamique (comparaison à laquelle j'ajoutais si je peux m'exprimer ainsi) vient du fait que lorsque l'on prend un énoncé universellement quantifié de la théorie, on quantifie sur tout l'univers des ensembles qui se comporte alors à la manière du
interface{}du Go. ;-) Raison pour laquelle les auteurs de HoTT écrivent en introduction de leur ouvrage :Ce que j'ai graissé est à mettre en lien avec les reproches adressées à Go d'utiliser le
interface{}pour la généricité du code, ce qui ne permet pas de garantir statiquement l'homogénéité d'une liste : il faut écrire des fonctions de constructions qui font du typage dynamique à base de switch sur les types des paramètres.Ceci est à mettre en parallèle avec les énoncés que l'on ferait sur l'encodage des entiers naturels dans ZF, où on écrirait
pour énoncer une propriété des entiers. Ici le quantificateur universel sur
xparcourt la collection de tous les ensembles (intreface{}) puis l'énoncé est une proposition hypothétique dont l'antécédent $x \in \omega$ correspond à une vérification dynamique de type avant de continuer « l'exécution » vers le conséquent. Je vois alors l'énoncé comme une fonction qui prend en entrée uninterface{}et qui fait du typage dynamique : une assertion de type ou un switch (comme tu veux), comme en Go. En Coq ou en HoTT, on écrirait tout simplementforall (x : Nat) ..., soitpour tout entier, .... La notion de type capture bien mieux que celle d'ensembles (au sens de ZF) la notion logique de concept.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
Sommaire
Kant et les théories des types
Ce que tu me demandes (infirmer la chose) est impossible à effectuer dans un commentaire. Tout ce que je peux dire c'est que les liens entre la philosophie kantienne et les théories des types contemporaines sont une évidence pour qui les connaît : elles procèdent toutes de la même approche méthodologique.
Le mieux que je puisse faire dans un commentaire, c'est pointé du doigt quelques références : Per Martin-Löf et Jean-Yves Girard.
Le second est l'auteur, entre autre, du système F qui est un système de types génériques pour le lambda-calcul : c'est le système de type à la base de langages comme Haskell ou OCaml. Sur sa page personnelle (le lien est sur son au-dessus) tu trouveras une partie intitulée La syntaxe transcendantale :
Le livre en question (le fantôme de la transparence) est celui dont j'ai parlé à gasche dans ce commentaire. Je ferais deux remarques là-dessus. Le qualificatif transcendantale est une référence on ne peut plus explicite à Kant, ce dernier ayant utilisé les expressions philosophie transcendantale ou philosophie critique pour qualifier son œuvre philosophique. Ensuite, à la fin de l'introduction du livre, on peut lire :
En ce qui concerne Martin-Löf, il est également l'auteur d'une théorie de types dépendants intuitionnistes. Il a participé au groupe de travail ayant écrit la théorie homotopique des types (HoTT) visant à fournir une alternative à ZF pour le fondement des mathématiques basée sur la théorie des types (ça se comprend, ZF c'est l'archétype du typage dynamique; il n'y a qu'un seul type statique : celui d'ensemble, tout le reste est dynamique, si je peux m'exprimer ainsi). Dans l'introduction du livre HoTT, on lit :
Martin-Löf est aussi l'auteur d'un article : analytic and synthetic judgements in type theory sur la philosophie kantienne des mathématiques. De même l'omniprésence de Kant dans la première des trois conférences qu'il donna sur la logique en 1983 à Siena devrait te mettre sur la piste.
Lorsque l'on s'occupe à notre époque de théorie des types, éluder toute référence kantienne pourrait s'apparenter, pour reprendre une expression utilisée ailleurs dans les commentaires, à une faute professionnelle.
Kant et la physique théorique
Je n'ai pas écouté la conférence mais seulement lu le texte qui l'accompagne. Je ferais deux remarques là-dessus :
Kant et les kantiens ne pratiquent pas de science expérimentale mais de la science pure ou rationnelle, c'est-à-dire des sciences dont les principes fondamentaux ne sont pas fondés sur l'expérience et l'observation, et dans les sciences expérimentale ne considèrent que la forme nécessaire que doivent prendre leurs théories pour être adéquate à la structure de notre esprit. Tu noteras que je parles d'esprit et non de cerveau : le cerveau est aussi peu le siège de la pensée que le cœur est celui des émotions, si ce n'est par amalgame matérialiste. Dans un tel champ du savoir, le recours aux hypothèses est mal venu :
Avoir recours à des hypothèse dans ce genre d'enquête, ce serait comme vouloir fonder la mathématique sur des conjectures : ce n'est pas sérieux.
Maintenant, comme exemples de personnes ici du monde de la physique ayant écouté l'appel de Kant, je citerai :
J'ajouterai simplement qu'une telle situation n'a rien d'étonnant quand on connaît certaines résultats de la physique quantique et le contenu de la philosophie kantienne. Je conclurai sur la réponse d'un kantien à un extrait du livre d'Étienne Klein :
Ce qui choque un Kantien n'est pas ce qu'il dit des objets quantiques, mais ce qu'il dit de la pierre ! :-P
Les objets que nous observons, en tant qu'objets de la connaissance expérimentale, n'ont aucune existence propre indépendante de nous. Si nous voyons partout de l'espace et du temps dans l'expérience, c'est parce qu'on les y met nous-même (voir l'article de Thibault Damour). Ainsi, lorsque l'on fait abstraction de tout rapport à l'expérience possible alors l'espace et le temps s'évanouissent, ce qui nous apparaît comme une pierre dans l'expérience devient un quelque chose d'inconnu, qui nous restera à jamais inconnaissable, une chose ineffable (dont on ne peut parler). L'avantage du kantisme sur toute autre approche épistémologique est qu'il ne fait aucune distinction ontologique entre la pierre et les objets quantiques : ce ne sont que de simples phénomènes qui n'ont pas d'existence propre en dehors de leur rapport à un observateur.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2. Dernière modification le 27 octobre 2017 à 15:28.
Pas spécialement, le principe que je décris est celui qu'a utilisé Gödel pour démontrer son fameux théorème d'incomplétude : une théorie assez riche (au pouvoir expressif suffisant) pour parler d'elle même a toujours des énoncés indécidables (qu'elle ne peut ni prouver ni réfuter) et parmi ceux-ci figurent toujours sa propre cohérence (sa non contradiction). Ce que je dis c'est que si une théorie est assez riche (comme l'est ZF) pour exprimer les principes de la théorie des modèles et donc parler de la relation entre la forme et le contenu (ce en quoi consiste la vérité) alors elle ne peut engendrer son propre contenu (elle ne peut construire un modèle d'elle même) et fournir un critère matériel et universelle de la vérité, sous peine d'être incohérente d'après le théorème d'incomplétude. Dans ce cas, comme elle peut prouver tout et n'importe, on ne peut nullement avoir confiance dans ce qu'elle prétend affirmer.
Cette démarche consiste à réfléchir la métathéorie dans la théorie elle même, c'est le même genre d'argument qu'a utilisé Turing pour prouver l'impossibilité de résoudre le problème de l'arrêt pour sa machine universelle. D'un point de vue programmation, cela revient à dire qu'un langage ne peut se compiler lui-même sans une phase de bootstrap : il faut un coup de pouce extérieur au langage de programmation.
L'univers des constructibles de Gödel sert à prouver des théorèmes de consistance relative : si ZF est non contradictoire alors il en est de même de ZF augmentée de l'axiome du choix, ce dernier axiome n'introduit pas de contradiction dans la théorie. C'est du même ordre que les théorèmes de consistance relative que Poincaré a effectués au XIXème entre les géométries euclidienne et non euclidiennes. Le cercle de Poincaré, construit dans un espace euclidien, permet d'interpréter les axiomes de la géométrie hyperbolique. Autrement dit, si la géométrie euclidienne est cohérente alors il en est de même de l'hyperbolique.
En revanche aux questions : l'arithmétique est-elle cohérente ? la géométrie est-elle cohérente ? ZF est-elle cohérente ? la logique et son principe de contradiction est incapable d'y répondre. La seule chose qu'elle peut faire c'est prouver la cohérence d'une théorie en admettant la cohérence d'une autre. Par exemple, on peut prouver la cohérence de l'arithmétique à partir de ZF, mais reste la question : ZF est elle cohérente ? On peut continuer en ajoutant des axiomes de grands cardinaux qui prouvent la consistance de ZF (ils fournissent un modèle de celle-ci), mais reviens alors la question : ses nouveaux axiomes sont-ils cohérents ? Et cette approche turtles all the way down la logique formelle ne peut en sortir, pour la simple raison que, laissée à elle même, elle n'engendre que des tautologies (l'art de M. de La Palice) et est incapable de répondre à la question : comment des jugements synthétiques a priori sont-ils possibles ?
Ça se discute, ils ne sont nullement enrichis, ce sont les mêmes mais exprimés dans une langue différente. Un principe ne deviendrait ni plus vrai, ni plus clair, ni plus riche sous prétexte qu'il serait exprimés en français plutôt qu'en anglais (ou vice versa). La méthode kantienne est on ne peut plus formelle (il n'y a pas plus formaliste qu'un kantien), et les langues naturelles sont tout à fait adaptées pour exprimer de tels principes. Il n'est pas nécessaire de recourir à des symbolismes compréhensibles par une machine (ce qui n'est d'ailleurs adapté qu'à la formalisation de la pensée mathématique mais nullement à la pensée philosophique, comme les problèmes de philosophie du droit) pour formaliser sa pensée : je préfère de loin l'usage du français à Coq, par exemple. Les langues naturelles ont, en leur sein, un système à type dépendant mais une grammaire plus complexe que les grammaires régulières des langages de programmation (il suffit de voir la difficulté que rencontre l'auteur de grammalecte, ou tous ceux qui travaillent sur le traitement automatique des langues).
Prenons, un principe de base de la logique de Hoare utilisée pour la formalisation des langages impératifs, celui de la composition des instructions :
une expression de la forme
{ P } S { Q }se lit : l'instructionSfait passer le système de l'étatPà l'étatQ. Une telle règle ce lit alors : si l'instructionSfait passer la machine de l'étatPà l'étatQet que l'instructionTfait passer de l'étatQà l'étatR, alors la série d'instructionsS ; Tfait passer de l'étatPà l'étatR.Il se trouve que c'est l'analogue dans le paradigme de la programmation fonctionnelle pure de la composition des fonctions :
Autrement dit, des deux prémisses
si A alors Betsi B alors C, on conclue àsi A alors C. Cela résulte d'une double application de la règle dite du modus ponens :ainsi en supposant A on conclue à C, c'est à dire que l'on a prouvé
si A alors C. Ce genre de preuve, quelque peu pédante, est ce que nous oblige à écrire Coq (il offre quand même des techniques pour éviter de rentrer autant dans les détails).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 et qu'il a pour type (là j'emploie une terminologie contemporaine) la forme logique des jugements hypothétiques (
si A alors B).On pourrait exprimer le principe fondamentale de la dynamique de Newton ainsi dans un tel symbolisme :
{ p } F { p + F * dt}. Autrement dit, un corps dans l'état de mouvementpet soumis à une forceFse retrouve dans l'état{ p + F * dt }au bout d'un temps infiniment petitdt. L'on retrouverait ainsi les considérations entre les sémantiques petit pas (small step) ou grands pas (big step), auxquelles gasche faisait allusion dans ce commentaire, et la distinction entre les lois différentielles et les lois intégrales en physique théorique. La première étant une approche discrète (sémantique des langages de programmation), là où la seconde est continue (physique théorique).Et c'est ce lien formel entre le principe de causalité et la forme des jugements hypothétiques qui explique que l'on peut construire des machines qui « exécutent » les calculs automatiquement.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2. Dernière modification le 27 octobre 2017 à 09:41.
Oui car telle est son affaire, elle peut montrer l'incohérence d'une formalisation. Pour ce qui est de prouver la cohérence, par contre…
Ça me rappelle ce passage humoristique dans la partie remerciements de la thèse de Perthmâd (qui, s'y j'en crois les notes de publication de la toute récente dernière version de Coq, a fait un gros travail de nettoyage et d'optimisation du langage des tactiques) :
Dans une démarche également historique, le passage que j'ai cité de la Critique de la Raison Pure est extrait du paragraphe sur la question « Qu'est-ce que la vérité ? » qui commence ainsi :
On trouve des considérations identiques dans le traité qu'il consacra à la logique. Premièrement, ce qu'il appelle la définition nominale de la vérité est celle que l'on utilise toujours de nos jours sous le nom de définition tarskienne de la vérité à la base de la sémantique tarskienne (utilisée en théorie des modèles). Ensuite, si l'on combine le théorème de Gödel auquel Perthmâd fait allusion (le théorème d'incomplétude) à une autre théorème fondamentale de Gödel (son théorème de complétude : une théorie est cohérente si et seulement si elle a un modèle), on aboutit à la conclusion du texte kantien cité ci-dessus. Une théorie (disons ZF, la théorie axiomatique des ensembles) qui fournirait un critère matérielle de sa vérité serait en mesure d'engendrer son propre contenu (fournirait un modèle d'elle-même), serait donc cohérente (en vertu du théorème de complétude) ce qui contredirait le théorème d'incomplétude.
Le théorème d'incomplétude clos une période historique au cours de laquelle la thèse centrale de la Critique de la Raison Pure fut attaqué de toute part par des logiciens, et Gödel finit par donner raison à Kant. :-)
À cette subdivision de la question, précède le texte suivant :
Ce qu'a prouvé Gödel, c'est que la logique formelle (et donc le principe de contradiction) ne peut légitimer à elle seule le raisonnement par récurrence : le principe du raisonnement par récurrence est un pur jugement synthétique a priori.
Il y a un membre de linuxfr qui a pour signature quelque chose du style : «BeOS le faisait déjà il y a vingt ans ». Pour ma part, d'une manière générale, je dirais : ce que font les théories des types contemporaines, Kant le faisait déjà il y a plus de 200 ans. Par exemple, la logique de Hoare utilisée par frama-c, c'est dans la Critique de la Raison Pure; ou bien la programmation par contrat, la gestion de propriété des espaces mémoires par Rust ou Mezzo, c'est dans la Doctrine du Droit (que l'on peut voir comme une théorie de typage du droit romain). :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Possibilité d'éditer ses propres contenus
Posté par kantien . En réponse à la dépêche Améliorons l’expérience utilisateur de LinuxFr.org !. Évalué à 4.
Tu sous-entend que pasBillpasGates devrait administrer un serveur mail et offrir une adresse à chaque membre de linuxfr ? :-D
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
Petit ajout que j'ai oublier de préciser avec le type contradictoire.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2. Dernière modification le 25 octobre 2017 à 09:32.
C'est type-safe le
interface{}, c'est un type existentiel. Par contre tu perds la garantie du typage statique et tu dois faire des assertions de type ou du switch sur type : il faut faire du typage dynamique. C'est comme en Python, en somme, sauf qu'en dehors deinterface{}on a bien la garantie d'un typage statique (sans quantification universelle sur les types, c'est-à-dire, sans généricité mais c'est déjà pas trop mal). En gros, je le vois comme ça (je me trompe peut être) :mais comme Go garde des informations de typages au runtime, on peut retrouver à l'éxecution la valeur contenue dedans avec son type : pour Go,
iest de typeintet vaut1.Ce qui n'est pas type-safe, c'est une valeur de tout type (avec quantification universelle sur les types). On parle de l'aspect unsound du système de type de Java (qui a des génériques) ou de la valeur
undefinedde Haskell ?Là, on contourne clairement le système de types, mais on annonce la couleur en utilisant le module
Obj. ;-) Le type defaux, c'est le principe ex falso quodlibet.Par contre j'ai un peu trop surestimé le système des interfaces : j'ai cru que c'était du type classes à la Haskell mais sans types paramétriques. En fait non, c'est clairement moins bien fait, tu ne peux pas avoir d'interface pour de telles méthodes :
On ne peut pas définir le type
interfacede ceux qui implémentent la méthodeAdd: c'est nul et ça pourrait limiter le besoin de recourir àinterface{}. Déjà qu'il n'ont pas de génériques (types paramétriques), ils auraient pu faire un effort de ce côté là.En OCaml :
Le mécanisme des arguments implicites (s'il était implémenté) permettrait d'inférer automatiquement le
'a addà utiliser en fonction du type'ades autres paramètres passés àaddpar unification, là où pour l'instant on doit le passer explicitement (c'est ce que font les types classes de Haskell mais en plus général, les types pouvant être paramétriques comme avec les monades). Go fait cela mais de manière très restreinte : la variable de type'tne doit pas apparaître dans le type des champs de l'enregistrement. /o\Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
Je sais bien que tu n'ignores pas les exigences en question, mon conseil de visionnage était là pour te dire que Xavier Leroy non plus, que son projet s'inscrit dans cette démarche d'exigence (raison pour laquelle il aborde le secteur de l'aéronautique), et que tu pourras peut être comprendre en quoi ce logiciel est une avancée dans la recherche de sécurité par rapport aux méthodes antérieures — celles que tu connais déjà, justement.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 5.
Je crois bien que le ton de nos échanges est monté par ma faute, j'en suis désolé. J'étais mal luné l'autre jour, j'aurais du tourner mes doigts dix fois avant d'écrire, j'en suis désolé. :-/
Tout à fait, mais cette problématique est hors de portée de la logique et des approches formelles.
La partie graissée correspond à ce que tu dis : si l'erreur est dans le modèle (le contenu, la matière), la logique qui ne s'occupe que de la forme ne peut rien y faire. Pour grossir le trait, la logique n'a rien à reprocher au raisonnement suivant :
celui qui se croirait immortel, en se justifiant du fait que la logique ne trouve rien à redire à ce syllogisme, ferait rire n'importe qui face à lui. :-D
Pour faire une analogie avec le domaine juridique : la logique s'occupe des vices de forme dans la procédure. En l'absence de vice de forme, il faut tout de même un procès pour débattre de l'issue du cas : on y examine la question de droit (la majeure du raisonnement : les hommes sont immortels) et la question de fait (la mineure du raisonnement : je suis un homme). Ici, la majeure est en tort : l'accusé est innocenté, déclaré non coupable, ou plutôt non immortel. La question de fait en revanche ne fait ici pas de doute; en cas de non lieu c'est celle-ci qui n'a pu être justifiée.
Tout à fait : c'est bien pour cela que je parlais d'un travail de titan ! Il faut formaliser les instructions assembleurs (de trois architectures qui plus est : PowerPc, ARM et x86), formaliser la sémantique d'un sous-ensemble assez large du C, puis prouver que toutes les transformations-traductions du code préservent les sémantiques. Mais Xavier Leroy et son équipe on pu réaliser cet exploit (car s'en est un, une première au monde pour un compilateur) parce qu'ils avaient déjà un forte expérience dans l'écriture de compilateur et de sémantique des langages de programmation : ils en avaient entrepris auparavant une étude approfondie en dehors de la logique. ;-)
Nulle condescendance dans mon message, je mets cette réaction sur le dos du ton que prenaient nos échanges. Je ne suis pas sans savoir comment cette question est gérée en l'absence d'un tel outil, mais je tiens à signaler que la garantie que CompCert apporte sera à jamais inaccessible à ces méthodes. Raison pour laquelle Gérard Berry, qui n'ignore pas non plus ces méthodes, a écrit :
Le graissage est de moi pour bien souligner que les méthodes auxquelles tu fais allusion, si elle sont acceptées en pratique, ne pourront jamais apporter ce niveau de garanti (j'espère que tu m'épargneras un débat épistémologique sur la distinction entre la connaissance rationnelle et la connaissance expérimentale afin de justifier cette position).
Je tiens à préciser à nouveau que ce compilateur fait partie de la chaîne d'outils que AbsInt vend à ses clients dont Airbus. :
Bien sûr que j'ai le compris : un tel outil doit savoir cacher ses entrailles pour exposer à l'utilisateur ses concepts métiers pour qu'il se focalise sur ce qu'il connaît. Il n'empêche que sous le capot, c'est de la traduction mathématique et de la preuve mathématique, quand bien même l'utilisateur n'en a pas conscience. Un bon outil est celui qui sait se faire discret sur son fonctionnement : celui qui l'utilise, celui qui le construit et celui qui le répare sont rarement les mêmes personnes, n'ont pas les même savoir, ni les mêmes compétences.
D'ailleurs pour illustrer la chose : je ne connaissais pas Go, si ce n'est de nom. Résultat je suis allé jeter un coup d'œil, et bien je trouve leurs choix tout sauf bêtes contrairement à ce que certains ont pu dire. Il n'y a certes pas de généricité (sauf sur quelques types comme les tuples ou les tableaux) mais leur système de type
interfaceest très ingénieux et semble compenser allègrement à l'usage l'absence de généricité. D'un point de vue formel, au premier abord (je n'ai pas creusé plus que cela) ça s'apparente grandement à des fonctions avec arguments implicites sur du lambda-calcul simplement typé avec enregistrements (un langage avec des fonctions comme citoyen de première classe pour lequel un argument de certaines fonctions est inférer par le compilateur)1. Le polymorphisme au lieu d'être paramétrique (comme C++, Java, Haskell…) et ad-hoc mais vérifier à la compilation. Choix qui offre aux développeurs un large panel de technique de programmation sans l'assomer avec des abstractions difficiles à comprendre, donc à maîtriser et donc à utiliser (comme le sont les modules ou les GADT pour toi).Haskell a cela avec ses type classes, mais OCaml manque d'un tel dispositif ce qui rend un code qui fait un usage intensif de modules très vite incompréhensible pour celui qui n'en est pas l'auteur. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: go 2.0
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3. Dernière modification le 21 octobre 2017 à 15:10.
On en revient toujours au fait que les modules implicites seraient une fonctionnalité géniales pour OCaml. Elle rendrait les modules encore moins citoyen de seconde classe que ne le font les first-class modules. ;-)
Lorsque j'avais mentionné à Leo White l'article-tutoriel sur les structures canoniques en Coq, il m'a répondu l'avoir déjà lu (effectivement, cela fait même partie des références de l'article de présentation du prototype sur les modules implicites). Cela étant, ils mentionnent un autre article intéressant, qui pourrait servir de base pour la formalisation, dans leurs références : The Implicit Calculus: A New Foundation for Generic Programming qui mentionne aussi le tutoriel sur les structures canoniques. Mais il me vient à l'esprit une interrogation :
S'il est vrai que dans sa thèse il décrit un algorithme d'unification plutôt qu'une formalisation à base de règles d'inférence à la Gentzen, les deux approches ne me semblent pas si éloignées et je ne vois pas ce qu'il manque à ce système pour fournir ce dont ont besoin les modules implicites pour synthétiser les arguments implicites.
Dans un autre registre, sur le statut des modules dans le langage : que penses-tu des travaux de Rossberg, Russo et Dreyer sur 1ML présentés à l'ICFP en 2015 ? Cela demanderait trop de modifications à apporter au langage pour avoir cela dans OCaml ?
et ça résoudrait les incompréhensions de Nicolas Boulay, ils y définissent les modules avec la syntaxe des enregistrements. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4. Dernière modification le 21 octobre 2017 à 00:41.
Bien sur que non, c'est un travail de titan le code complet ! C'était pour illustrer ma proposition « la quantité d'erreurs attrapées à la compilation dépend de l'expressivité du système de types », en montrant un système de types tel que son expressivité dispense d'avoir à recourir à des tests unitaires. Ce théorème, qui n'est qu'une infime partie du code du compilateur, est celui que Xavier Leroy utilise dans sa vidéo comme illustration : c'est normal, c'est lui qui exprime que son compilateur est optimisant est n'apporte aucune modification de comportement à la compilation (si il y a un problème dans le code compilé, il se trouve déjà dans le code C).
Je le sais bien, c'est pour cela que j'ai parlé de cette industrie. Au sujet du projet CompCert C, Gérard Berry (lui, tu le connais il a cofondé l'entrepise qui fut (est ?) ton employeur et est le père du langage Esterel) l'a décrit dans le bulletin de la société informatique de France ainsi :
Pour info le compilateur est un produit (il n'est pas libre, seulement pour un usage non-commercial) de l'entreprise AbstInt :
qui a pour client Airbus et pour partenaire Esterel Technologies. ;-) Pour Airbus, ils utilisent leurs analyseurs statiques de code (aiT analyse le comportement temporel, StackAnalyzer l'absence de stack overflow et Astrée l'absence de runtime error) :
et Compert C s'incrit dans la chaîne des outils : si le code C est propre et garanti c'est bien, mais si le compilateur introduit un bug c'est un peu couillon, tu ne crois pas ?
T'es sûr ? Tu faisais (ou fais) quoi comme travail chez Esterel ? Tu y appris quoi chez eux pour avoir écrit cela ?
T'as pas compris depuis le temps que ce tu qualifies de "industrielles", ce sont aussi des preuves de matheux ? ;-)
Tu devrais tout de même jeter un œil à la vidéo de Xavier Leroy dont j'ai donné le lien au-dessus, il y parle pendant une vingtaine de minutes du milieu de l'avionique et de ses exigences de certification.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.