Je répondais à quelqu'un qui disait que les tests unitaires étaient limités par rapport au raisonnement mathématique. Sauf qu'en vrai on a introduit les test unitaires parce que le raisonnement mathématique était limité (pas impossible, mais insuffisant).
Et je maintiens mes propos, sauf qu'on a introduit les tests unitaires parce que l'automatisation totale du raisonnement mathématique était limitée (on le savait déjà depuis Gödel, Rice n'est qu'une variante sur le même thème). Ce qui n'empêche pas de mettre en place des systèmes formels d'aide à la preuve où une partie est faite automatiquement par la machine, ou celle-ci aiguille le développeur qui effectue ce que la machine ne fait pas seule, et cela dans un langage où le système de type est bien plus expressif sur la sémantique du code (Coq en est l'exemple type).
Sans automatisation, en général les gens ne vont pas s'embêter à démontrer que le programme est correct car les preuves sont bien plus complexes que l'écriture de programme.
Cela dépend de l'aspect critique du programme, c'est comme pour tout il faut choisir l'outil adapté à ses besoins : on ne sort pas un char d'assaut pour écraser une mouche. Je n'ai jamais dit qu'utiliser des langages avec un expressivité sémantique limitée qui exigeait le recours aux tests unitaires étant sans intérêt, mais que des besoins pouvaient trouver cette approche insatisfaisante surtout que l'on sait faire plus sûr.
Ou encore tu pourrais expliquer l'inutilité (on va pas s'embêter à faire ça) de ce genre d'approche aux clients de AbsInt : Airbus, Esa, Nasa, Areva, Infineon, Continental, Thales, Bosch, BMW, Nokia, T-Systems, Intel, Compaq, Alliance Spacesystems, IBM, Sagem, Baxter, Healthcare Sanyo, Hewlett-Packard... perdre du temps est sans doute leur objectif premier.
Et on ne fait pas cela que sur des petits programmes, pour répondre au cas Arianne 5 et Rover, un compilateur C ce n'est pas ce que j'appelle un petit programme, mais Xavier Leroy doit lui aussi aimer s'embêter et perdre son temps.
Désolé mais je suis mon conciliant que gasche : ton utilisation du théorème de Rice est fumeuse.
(* le premier je le fais en deux temps *)letrecfx=fx;;valf:'a->'b=<fun>(*puis la je l'applique sur unit mais on peut prendre n'importe quoi *)f();;(* jolie boucle infinie, on fait Ctrl-C *)(* le second je le code en OCaml *)(* la fonction identité c'est la tautologie A ⇒ A *)letidx=x;;valid:'a->'a(* maintenant j'en fait une version restreinte avec un type fantôme *)typefaux;;letf(p:faux)=p;;valf:faux->faux
Le problème avec f serait de pouvoir l'appliquer (en faire usage) c'est à dire de pouvoir produire un terme de type faux alors que celui-ci est sans constructeur donc vide (ou inhabité).
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 1.
Et je maintiens mes propos, sauf qu'on a introduit les tests unitaires parce que l'automatisation totale du raisonnement mathématique était limitée (on le savait déjà depuis Gödel, Rice n'est qu'une variante sur le même thème). Ce qui n'empêche pas de mettre en place des systèmes formels d'aide à la preuve où une partie est faite automatiquement par la machine, ou celle-ci aiguille le développeur qui effectue ce que la machine ne fait pas seule, et cela dans un langage où le système de type est bien plus expressif sur la sémantique du code (Coq en est l'exemple type).
Cela dépend de l'aspect critique du programme, c'est comme pour tout il faut choisir l'outil adapté à ses besoins : on ne sort pas un char d'assaut pour écraser une mouche. Je n'ai jamais dit qu'utiliser des langages avec un expressivité sémantique limitée qui exigeait le recours aux tests unitaires étant sans intérêt, mais que des besoins pouvaient trouver cette approche insatisfaisante surtout que l'on sait faire plus sûr.
Sinon, tu devrais en toucher deux mots à Gérard Berry dont les cours des deux dernière années au Collège de France ont été sur les thèmes : Prouver les programmes : pourquoi, quand, comment ? et Structures de données et algorithme pour la vérification formelle.
Ou encore tu pourrais expliquer l'inutilité (on va pas s'embêter à faire ça) de ce genre d'approche aux clients de AbsInt : Airbus, Esa, Nasa, Areva, Infineon, Continental, Thales, Bosch, BMW, Nokia, T-Systems, Intel, Compaq, Alliance Spacesystems, IBM, Sagem, Baxter, Healthcare Sanyo, Hewlett-Packard... perdre du temps est sans doute leur objectif premier.
Et on ne fait pas cela que sur des petits programmes, pour répondre au cas Arianne 5 et Rover, un compilateur C ce n'est pas ce que j'appelle un petit programme, mais Xavier Leroy doit lui aussi aimer s'embêter et perdre son temps.
Désolé mais je suis mon conciliant que gasche : ton utilisation du théorème de Rice est fumeuse.
Pour rebondir sur les deux exemples que t'a donné Burps.
Le problème avec
fserait de pouvoir l'appliquer (en faire usage) c'est à dire de pouvoir produire un terme de typefauxalors que celui-ci est sans constructeur donc vide (ou inhabité).Le second exemple porte un nom de sophisme bien connu : la pétition de principe, le premier étant le raisonnement circulaire qui n'en est qu'une variante. :-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.