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.
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.
Globalement la qualité se résume souvent à un cahier de tests, avec des tests unitaires ou fuzzing sans oublier la revue de code et l'intégration continue. Quand tu as ça, déjà, tu es content.
À l'époque, les deux seuls langages que l'ont m'a enseigné était OCaml et Coq
Juste pour préciser, très peu d'ingénieurs en France et Belgique (et je pense que c'est plus ou moins pareil partout pour des ingés niveau master) voient dans le cadre scolaire les langages fonctionnels de manière sérieuse. Alors Coq et OCaml tu comprendras que ta formation est assez décalée de ce que rencontre la plupart des développeurs.
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 :
Je pense que personne ne va te contredire sur ce point, d'ailleurs Knuth a une citation sur le sujet. Mais il me semble naïf de croire que cette méthode soit viable et générique, en tout cas aujourd'hui.
Je veux dire, en général cette artillerie est réservée vraiment à des domaines de haute criticité où le rapport bénéfice / coût est évident. Typiquement en aéronautique cela sera exigé / recommandé pour les DAL A ou B, mais pas au delà. Et les coûts d'un tel travail est tel que c'est rarement appliqué en dehors de ces contextes là. Qui d'ailleurs reposent sur du matériel et du logiciel simple, élémentaire pour faciliter ce travail. Voire le rendre possible, car si je ne me trompe pas, tu ne peux pas prouver formellement que n'importe quel programme fonctionnera tel qu'attendu.
D'autant que si ton programme a un lien fort avec ton matériel (cas du noyau ou d'un logiciel embarqué), il faut aussi formaliser le matériel et cette liaison. Est-ce que des processeurs ou GPU modernes bénéficient d'un tel travail ? J'en doute.
je tombe des nues. :-O Mais enfin, c'est une évidence pour qui est un minimum rigoureux intellectuellement !
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é.
Et encore, c'est en supposant que le travail soit gratuit, ce qui ne l'est bien évidemment pas vrai. Car c'est bien de venir avec une théorie, une idée, il faut quelqu'un pour le mettre en œuvre, le maintenir et que cela ne gêne pas les autres développeurs. Typiquement si tu viens avec un système d'annotation du code, qui pourrait apporter un gain pour l'analyse du noyau. Il faut que quelqu'un annote tout le code existant, documente cette section et que les autres développeurs exploitent cela. C'est un travail titanesque et potentiellement ingrate. Même si le gain sur le long terme est démontré, il faut encore que quelqu'un ou une entité investisse dedans et ce n'est rien d'évident. Surtout que pendant la période de transition tu risques d'avoir des pertes de productivité importantes aussi.
Bref, tout dépend, mais il faut tenir compte de ces éléments aussi dans l'aspect "démonstration". La réalité a ses propres contraintes qui peuvent rendre difficile la transposition recherche théorique / logiciels industriels.
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 ?
La communauté ne s'en moque pas, la question de la qualité du noyau est de plus en plus centrale dans les discussions. Cela passe par l'intégration continue, le fuzzing, les tests unitaires, etc. qui se généralisent.
Mais la communauté du noyau n'a pas d'exigence particulière non plus. Selon la communauté avec qui tu parles, la sécurité doit être le critère 1, ici ça parle plutôt de l'analyse et de la conformité du code, pour d'autres ce sera la performance, etc. La communauté du noyau le cherche pas l'excellence dans tous les domaines à la fois (ce n'est pas réaliste) mais un compromis.
De la même façon qu'aujourd'hui tu n'as aucun micro-noyau pur utilisé massivement pour une large gamme d'utilisation. Car si la théorie est belle, les contraintes sont telles que le compromis impose soit de faire du monolithique modulaire (Linux, BSD) ou du micro-noyau enrichi (Windows, macOS, iOS). Pourtant Microsoft et Apple ne sont pas des brelles (ils ont des équipes de R&D à la hauteur), ils peuvent largement payer ou contraindre des employés de bosser sur la question. Et pourtant le résultat est contraire à la prédiction de la recherche du secteur depuis 25 ans.
[^] # Re: Le cerveau n'est pas logique
Posté par Renault (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 6.
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.
Globalement la qualité se résume souvent à un cahier de tests, avec des tests unitaires ou fuzzing sans oublier la revue de code et l'intégration continue. Quand tu as ça, déjà, tu es content.
Juste pour préciser, très peu d'ingénieurs en France et Belgique (et je pense que c'est plus ou moins pareil partout pour des ingés niveau master) voient dans le cadre scolaire les langages fonctionnels de manière sérieuse. Alors Coq et OCaml tu comprendras que ta formation est assez décalée de ce que rencontre la plupart des développeurs.
Je pense que personne ne va te contredire sur ce point, d'ailleurs Knuth a une citation sur le sujet. Mais il me semble naïf de croire que cette méthode soit viable et générique, en tout cas aujourd'hui.
Je veux dire, en général cette artillerie est réservée vraiment à des domaines de haute criticité où le rapport bénéfice / coût est évident. Typiquement en aéronautique cela sera exigé / recommandé pour les DAL A ou B, mais pas au delà. Et les coûts d'un tel travail est tel que c'est rarement appliqué en dehors de ces contextes là. Qui d'ailleurs reposent sur du matériel et du logiciel simple, élémentaire pour faciliter ce travail. Voire le rendre possible, car si je ne me trompe pas, tu ne peux pas prouver formellement que n'importe quel programme fonctionnera tel qu'attendu.
D'autant que si ton programme a un lien fort avec ton matériel (cas du noyau ou d'un logiciel embarqué), il faut aussi formaliser le matériel et cette liaison. Est-ce que des processeurs ou GPU modernes bénéficient d'un tel travail ? J'en doute.
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é.
Et encore, c'est en supposant que le travail soit gratuit, ce qui ne l'est bien évidemment pas vrai. Car c'est bien de venir avec une théorie, une idée, il faut quelqu'un pour le mettre en œuvre, le maintenir et que cela ne gêne pas les autres développeurs. Typiquement si tu viens avec un système d'annotation du code, qui pourrait apporter un gain pour l'analyse du noyau. Il faut que quelqu'un annote tout le code existant, documente cette section et que les autres développeurs exploitent cela. C'est un travail titanesque et potentiellement ingrate. Même si le gain sur le long terme est démontré, il faut encore que quelqu'un ou une entité investisse dedans et ce n'est rien d'évident. Surtout que pendant la période de transition tu risques d'avoir des pertes de productivité importantes aussi.
Bref, tout dépend, mais il faut tenir compte de ces éléments aussi dans l'aspect "démonstration". La réalité a ses propres contraintes qui peuvent rendre difficile la transposition recherche théorique / logiciels industriels.
La communauté ne s'en moque pas, la question de la qualité du noyau est de plus en plus centrale dans les discussions. Cela passe par l'intégration continue, le fuzzing, les tests unitaires, etc. qui se généralisent.
Mais la communauté du noyau n'a pas d'exigence particulière non plus. Selon la communauté avec qui tu parles, la sécurité doit être le critère 1, ici ça parle plutôt de l'analyse et de la conformité du code, pour d'autres ce sera la performance, etc. La communauté du noyau le cherche pas l'excellence dans tous les domaines à la fois (ce n'est pas réaliste) mais un compromis.
De la même façon qu'aujourd'hui tu n'as aucun micro-noyau pur utilisé massivement pour une large gamme d'utilisation. Car si la théorie est belle, les contraintes sont telles que le compromis impose soit de faire du monolithique modulaire (Linux, BSD) ou du micro-noyau enrichi (Windows, macOS, iOS). Pourtant Microsoft et Apple ne sont pas des brelles (ils ont des équipes de R&D à la hauteur), ils peuvent largement payer ou contraindre des employés de bosser sur la question. Et pourtant le résultat est contraire à la prédiction de la recherche du secteur depuis 25 ans.