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).
Je n'ai jamais dis qu'il était impossible de faire des maths ou de prouver des choses, même de manière formel. Je dis simplement qu'en pratique faire une preuve formel est très coûteux car relativement non automatisable.
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.
Après le problème vient aussi du fait qu'on a privilégié en informatique des langages de goret plutôt que langages propres. Pour un programme purement fonctionnel en OCaml, s'il passe la compilation sans warning on a la preuve qu'on n'aura pas d’erreur de typage à l'exécution et qu'on ne cherchera pas à accéder à des zones mémoires interdites. Dans cette optique par exemples les listes sont très supérieurs au tableau ou l'accès est toujours sources d'erreur potentiel. C'est pareil pour le concurrent, en remplaçant le partage de mémoire par le passage de messages, on a tout de suite moins de problèmes. De même lorsque l'on a remplacé les goto par des while/for/if.
OCaml donne automatiquement de nombreuses garanties sans que l'on ai besoin de faire les preuves soit même. Mais ce que dit Rice, c'est que les garanties données à la compilation (donc faites de manière automatique) sont toujours limitées à partir du moment où le langage est suffisamment expressif. Par exemple, le débordement de pile, la terminaison, sont sources d'erreur en OCaml.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par Diagonale de Cantor (site web personnel) . En réponse à la dépêche OCaml 4.03. Évalué à 5.
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).
Je n'ai jamais dis qu'il était impossible de faire des maths ou de prouver des choses, même de manière formel. Je dis simplement qu'en pratique faire une preuve formel est très coûteux car relativement non automatisable.
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.
Après le problème vient aussi du fait qu'on a privilégié en informatique des langages de goret plutôt que langages propres. Pour un programme purement fonctionnel en OCaml, s'il passe la compilation sans warning on a la preuve qu'on n'aura pas d’erreur de typage à l'exécution et qu'on ne cherchera pas à accéder à des zones mémoires interdites. Dans cette optique par exemples les listes sont très supérieurs au tableau ou l'accès est toujours sources d'erreur potentiel. C'est pareil pour le concurrent, en remplaçant le partage de mémoire par le passage de messages, on a tout de suite moins de problèmes. De même lorsque l'on a remplacé les goto par des while/for/if.
OCaml donne automatiquement de nombreuses garanties sans que l'on ai besoin de faire les preuves soit même. Mais ce que dit Rice, c'est que les garanties données à la compilation (donc faites de manière automatique) sont toujours limitées à partir du moment où le langage est suffisamment expressif. Par exemple, le débordement de pile, la terminaison, sont sources d'erreur en OCaml.