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