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.
[^] # 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.