Oui mais il y a alors une chose que je ne comprend pas, quand le programme doit interagir avec des données externes, il ne peut pas savoir "lors de la compilation" quelles valeurs il va recevoir en entrée. Par exemple, on fait x/y, pour tout y des lignes d'une table dans une base de données quelconque, il va bien falloir faire des tests non ?
Et une autre question que je me pose : un programme qui prend en compte tous les cas possibles, en traitant les problèmes par des tests, n'est-il pas en fin de compte lui-même "prouvé" ? Si on est sûr que tous les cas posant problème sont contournés, ce module peut être réputé sûr tout du moins, même si il ne s'agit pas de la notion de preuve.
Quand je disais que Math.divide(x,y) était plus précis que x/y, je parle surtout de l'analyse syntaxique, comme tu dis il est plus compliqué de traiter des expressions algébriques que de gérer des variables en paramètres dans une méthode, mais c'est encore une preuve de mon inexperience des compilateurs et des analyseurs syntaxiques, je trouve le problème infiniement complexe, par exemple :
x/(y/(z(1+x))) < comment traiter cette expression ?
Il est plus simple dans mon esprit de traiter :
Math.divide(x, Math.divide(y, Math.multiply(z, Math.add(1,x))));
Lorsque que tu dis que le constructeur doit se préoccuper de faire des freins qui ne lacheront pas, je dirais qu'on parle d'un domaine un peu différent, en mécanique il est vrai qu'on doit se soucier de fournir des éléments fiables, quitte à payer le prix fort pour les matériaux, car un défaut peut couter la vie. Et on ne peut pas mettre des capteurs partout pour détecter toutes les failles qui pourraient survenir. Ce serait impossible, car les paramètres ne sont pas tous connus.
C'est la différence entre le monde réel, constitué d'infines possibilités, et du monde informatique tel que je le vois, où le problème est différent, car le défaut est toujours de nature logicielle ( bien que le matériel peut aussi être responsable dans quelques cas, mais nous parlons du coté logiciel de la chose ) et donc pour contrer ce défaut il y a deux moyens pour rendre le logiciel sûr, les tests en temps réels, ou la fiabilité du "composant" logiciel utilisé. La deuxième solution, reviendrait à celle employée donc pour le cas de l'auto, une pièce fiable, mais cher ( ici en conception et en analyse ). Mais on a encore le cas peu couteux des tests, l'informatique offre l'avantage de fournir un moyen automatique de traiter les mêmes evenements, alors pourquoi ne pas appliquer ce principe à l'execution même d'un programme et à sa gestion d'erreur, en déployant une panoplie de tests, qui rendraient le code blindé de toute part ?
J'admire en tout cas le travail des gens comme toi, qui sont allés aussi loin dans l'abstraction, je propose une solution qui correspond à mes connaissances et à ce que je serais capable de produire, je ne dois sûrement pas encore réaliser la puissance de l'outil de preuve et le bienfait qu'il apporterait à l'informatique.. Dans le principe, un compilateur qui apporterait cette dimension de preuves, permettrait au developpeur de coder beaucoup de lignes de codes, en étant sûr que si la compilation a fonctionné, le programme sera garanti sans faille ? Ca me parrait inimaginable comme entreprise, mais je vois que tu es parmi ceux qui sont prêt à relever le défi et qui le prouvent par l'action, et encore une fois tu as toute mon admiration pour cette initiative
Partager