Il semble que mon point de vue se soit noyé dans les différents messages et ait été interprété plutôt à mon désavantage. Je vais donc essayer de le résumer :
J'utilise des méthodes formelles (en l'occurrence Coq) pour prouver mes programmes. Ces méthodes apportent une certitude proche de 100% que les programmes n'ont pas de bug. Ce que j'entends par là: déjà, ils n'ont pas de dépassement de tampon, pas d'overflow, pas de déréférencement de pointeurs nuls, pas de double free, etc. Là c'est plus le langage qui l'assure que vraiment la preuve. Ensuite, on sait qu'ils satisfont leur spécification (j'insiste sur le fait qu'on ne prouve pas un algorithme qu'on implémente ensuite. On prouve directement le programme).
Néanmoins, il reste toujours un risque d'erreur : une spécification erronée ou incomplète. Dans l'exemple que je donnais plus haut sur les optimisations, c'est une spécification incomplète (on demande à l'optimisation de ne pas altérer la sémantique du programme, mais on ne s'assure pas qu'elle optimise effectivement). Mais les spécifications sont écrite en langage mathématique, sans ambiguité, et sont (du moins dans l'idéeal) nettement plus concise que le programme les implémentant (voir la spécification de
add sur un AVL, comparée à son implémentation).
Il est enfin possible que l'outil lui même soit bogué, mais là, la probabilité est *vraiment* faible (la TCB (trusted computing base) est vraiment réduite)
Donc non, on n'est pas à 0% de chance d'avoir un bug, on est tout de même à beaucoup, beaucoup, beaucoup moins qu'avec des programmes non prouvés.
Néanmoins, ces méthodes sont extrêmement lourde à mettre en place. Il est par exemple très compliqué de prouver un programme impératif (surtout un programme C...). Rien que
spécifier un algo de tri (je ne parle même pas de le prouver), est une opération complexe (je parie mon poids en choucroute que la moitié des programmeurs sont incapable de donner une spécification correcte du premier coup). Alors prouver un quick-sort en place, boarf. Et en plus, ce n'est qu'une sous sous sous partie d'un vrai programme. Il y a donc encore un travail de titan à faire avant que ces méthodes soient accessibles au plus grand nombre.
D'ici là, je suis comme tout le monde, je veux continuer à voir l'informatique progresser et de nouveaux programmes arriver. Et dans ces programmes, il y aura toujours des bugs (puisqu'on n'a pas encore trouvé de programmeurs infaillible. La plupart reste humains...). Et donc oui, il faudra des outils pour aider à débuguer ! Bien sûr, le "good ol'" printf fonctionne dans plein de cas. Il me parait quand même bizarre de rejeter pour autant des outils un brin plus "moderne", comme un débogueur, surtout qu'ils ont quand même fait des progrès, principalement en terme d'interface !
Et puis il y a aussi une percolation progressive des différentes méthodes. Par exemple, le compilo C d'Apple incorpore un analyseur statique pour aider à trouver des causes classique d'erreurs. Tous ces outils permettent de limiter les cas où un déboguer est utile. Mais on est encore bien loin de le rendre inutile dans tous les cas.
8 |
2 |
Comment expliquez-vous que ces « masterminds » disent ne pas utiliser des débogueurs interactifs ?
Envoyé par spidermario
).:
, avec de vrais arguments techniques. Venez, on se concentre un peu là dessus ?
!
