Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter
Discussion :
Effectivement, étrange, d'autant plus que j'y étais après le changement orthographique du nom...
Mais effectivement dans ma branche, ça ne se justifiait pas forcément, ce qui m'étonne plus, c'est qu'on ne m'en ai pas parlé à Meudon ni à Massy!
Mais il est vrai que les cloisonnements sont assez étranges... surtout avec AT.
Bonjour à tous.
Je n'ai pas oublié que j'avais promis un petit comparatif entre preuves et programmes. Eh bien, le voici. D'abord, un petit rappel historique.
Le fait que les preuves sont des programmes a été sans aucun doute découvert en 1930 par Arend Heyting (un logicien Néerlandais), et ces questions ont été développées par lui, par L.E.J. Brouwer (maître de Heyting et initiateur de la logique intuitionniste) et par Kolmogorov. Le principe est connu sous le nom de 'sémantique de Heyting' ou encore 'interprétation de Brouwer-Heyting-Kolmogorov'.
Plus récemment, précisément en 1980, à l'occasion du 80ieme anniversaire d'Haskell Curry (le logicien dont le prénom est devenu le nom d'un langage fonctionnel), Howard a énoncé un principe connu aujourd'hui sous le nom d'Isomorphisme de Curry-Howard', qui stipule une parfaite similitude (isomorphisme) entre preuves et programmes. Cet isomorphisme de Curry-Howard (dans lequel Curry n'est pour rien d'ailleurs) me dérange un peu pour deux raisons. La première est qu'Howard a fait comme s'il inventait quelque chose de nouveau, alors que tout avait déjà été fait par Heyting 50 ans avant (rendons à César ce qui est à César), la deuxième est que prétendre qu'il y a 'isomorphisme' (c'est à dire similitude parfaite) entre preuves et programmes conduit à concevoir des systèmes formels dans lequels aucune notion correcte de sous-ensemble ne peut être définie. C'est un fait dont les logiciens et théoriciens de l'informatique commencent tout juste à prendre conscience aujourd'hui. Des langages avec preuve comme LEGO ou COQ souffrent de ce problème, qui rend quasiment impossible la manipulation de sous-ensemble ou d'ensemble quotients. Il faut donc abandonner l'isomorphisme de Curry-Howard. La théorie des topos donne une bien meilleure modélisation de ces questions. Mais ça c'est une autre histoire. Je vais quand même en toucher un mot à la fin de ce post.
Passons maintenant à la comparaison proprement-dite. D'un coté, en programmation, on a les notions de type et de terme (j'appelle 'terme', comme la plupart des logiciens, les expressions du langage qui représentent des données). Chaque terme a normalement un type. Evidemment, ici je me place dans le cadre d'un langage de programmation idéalisé. Dans les langages réels, il y a plein de notions supplémentaires qui viennent parfois en contradiction avec ce que j'expose ici. De l'autre coté, en mathématiques, on a les notions d'énoncé et de preuve (ou démonstration), qui sont à mettre en parallèle avec type et terme. Toute preuve correcte prouve un énoncé, de la même manière que tout terme correct a un type. D'ailleurs, l'un des slogans mis à la mode par Howard est 'formula-as-type', qu'on peut traduire par 'les énoncés vus comme des types'.
Les types (en dehors des types primitifs) sont construits selon divers procédés. Par exemple, dans la plupart des langages on a la notion de 'structure' (comme en C). Une structure est simplement un type dont chaque donnée est composée d'autant de données qu'il y a de types composants dans la structure. Une donnée d'un tel type est parfois appelée un aggrégat. En C bien sûr, tout cela est obscurci par le fait qu'on doit gérer la mémoire. Mais dans un langage de haut niveau, la notion de structure correspond exactement à celle de produit cartésien en mathématiques. Ce qui caractérise le produit cartésien de deux ensembles E et F est:
1. le fait qu'il y a deux projections (dites 'canoniques'): p1: ExF --> E et p2: ExF --> F
2. le fait que définir une application de X vers ExF consiste à donner ces deux composantes.
En langage C, les deux projections sont les noms des champs dans la structure, et le point 2 est réalisé par tout terme créant une donnée du type de cette structure.
En mathématiques, l'équivalent des types produits (structures) est la conjonction. Si E et F sont deux énoncés, on peut considérer l'énoncé 'E et F'. Les projections canoniques sont simplement les preuves (dont l'existence est appelée 'axiome') que de 'E et F' on peut déduire E et que de 'E et F' on peut déduire F. Le point 2 se traduit par le principe de démonstration qui veut que pour prouver 'E et F', on prouve d'une part E et d'autre part F. Ces deux preuves sont les deux 'composantes' de la preuve obtenue pour 'E et F', et l'ensemble X joue le rôle des hypothèses grâce auxquelles ces preuves sont écrites.
En fait, on peut rendre ce parallèle plus saisissant si on introduit la notion d'ensemble de preuves. Un ensemble de preuve est alors clairement un type dont les termes sont des preuves. Pour chaque énoncé, il y a un ensemble de preuves (qui est vide évidemment si l'énoncé n'est pas démontrable).
Il n'y a pas que les structures bien sûr comme constructeurs de nouveaux types. On peut considérer aussi les types fonctionnels. Là, je ne vais pas illustrer avec le langage C (qui n'est pas fonctionnel), mais avec Anubis (qui l'est), sinon tout cela risque de devenir fortement capillotracté. Si E et F sont deux types, on note E -> F le type des fonctions de E vers F. Ce qui caractérise un tel type (notez le parallèle avec les structures) est:
1. le fait que si le terme 'f' représente une fonction de E vers F, et 'a' un terme de type E, 'f(a)' est un terme de type F,
2. le fait qu'on peut construire des fonctions avec le symbole |-> (le même qu'en mathématiques, et qui n'est rien d'autre que le 'lambda' du lambda-calcul, ou encore le 'lambda' de LISP, ou le 'function' de JavaScript (qui est un langage fonctionnel !)).
'f(a)' s'appelle un 'terme applicatif', car il représente le résultat de l'application de la fonction 'f' à l'argument 'a'.
En mathématiques, l'analogue du type fonctionnel est l'implication. Si E et F sont deux énoncés, l'énoncé E => F (E implique F) joue pour E et F le rôle que joue le type fonctionnel E -> F pour les types E et F.
Le point 1. ci-dessus nous dit simplement que si 'f' est une preuve de 'E => F', et si 'a' est une preuve de 'E', alors 'f(a)' est une preuve de F. C'est un principe de démonstration bien connu (et complètement naturel, que tout le monde utilise sans s'en rendre compte, même dans les raisonnements de la vie courante). Les logiciens appellent ce principe 'modus ponens'.
Le point 2, nous dit que si on déclare une preuve de E (appelons-la 'x'), on peut construire une preuve de E => F de la forme x |-> K[x] (c'est à dire comme une fonction), où K[x] est une preuve de F contenant éventuellement des appels à x. Evidemment, en pratique, la flèche |-> (le 'lambda') s'écrit: 'Supposons que E', ce qui signifie en fait: 'Supposons que 'x' soit une preuve de E'. C'est ce qu'on appelle la 'méthode de l'hypothèse auxilliaire'. On verra un peu plus loin pourquoi les preuves sont déclarées implicitement (c'est-à-dire sans qu'on leur donne de nom précis).
Au point où nous en sommes, on peut faire un petit tableau comparatif.
On voit qu'à part le vocabulaire et les notations, c'est exactement la même chose. On pourrait traiter les autres connecteurs logiques ('ou', 'quelque soit', 'il existe') de la même manière. Ceux d'entre vous que cette question intéresse peuvent consulter la première de mes leçons de logique catégorique.
Code : Sélectionner tout - Visualiser dans une fenêtre à part
2
3
4
5
6
7
8
9
10
11
Voilà pour les ressemblances. Voyons maintenant les différences. Elles sont de deux sortes:
1. Celles qui résultent du principe de l'unicité du témoin,
2. Celles qui résultent du non déterminisme.
Le principe de l'unicité du témoin (qui à ma connaissance apparaît pour la première fois vers 1980, dans les travaux des logiciens Lambek et Scott) dit que deux preuves d'un même énoncé ont la même sémantique (représentent la même chose). Le vocable 'témoin' sert à nommer ce qui est représenté par une preuve, de même que le vocable 'donnée' sert à nommer ce qui est représenté par un terme.
Ce principe peut être justifié de deux façons. D'abord une façon disons 'naïve'. C'est un fait que les mathématiciens, dont l'une des quêtes est de trouver des preuves pour des énoncés, se contentent d'une preuve par énoncé. Ils ne font pas de distinction entre deux preuves d'un même énoncé, sauf sur le plan ergonomique, mais certainement pas sur le plan sémantique. C'est d'ailleurs la raison pour laquelle les preuves sont en général anonymes (non nommées). Du moment qu'on en a au moins une c'est bon. Nommer des choses n'est utile que pour les distinguer les unes des autres. Si vous êtes seul sur une île deserte, vous n'avez pas besoin de nom. Maintenant, il y a aussi des justifications théoriques, et la façon de définir les preuves en théorie des topos (chose qu'il m'est impossible d'expliquer ici, mais qui sera expliquée dans l'une de mes futures leçons de logique catégorique), entraine instantanément le principe de l'unicité du témoin.
Bien entendu, ce principe n'a pas d'équivalent pour les programmes, car il signifierait que deux termes de même type sont toujours égaux, autrement--dit que tout type contient au plus une seule donnée.
La deuxième différence entre preuves et programmes est due au fait qu'en informatique, on écrit des programmes 'interactifs' qui sont obligés de communiquer avec le monde réel. Ces programme ne sont pas de simples programmes de calcul abstrait (des boites noires), mais bien des robots (automates) avec des états dépendants du temps et du lieu. La programmation moderne est donc de facto non déterministe. A contrario, les preuves mathématiques sont complètement déterministes. Par exemple, je ne vois pas ce qu'une affectation de variable pourrait faire dans une preuve. A cause de cette obligation de prendre en compte des notions non déterministes, la programmation est dans ses principes beaucoup plus complexe que la démonstration. Maintenant, il est aussi possible de modéliser le non déterminisme avec des concepts mathématiques, mais cela aussi est une autre histoire.
En espérant que ce petit exposé vous ait éclairé, je vous recommande de toute façon, pour en savoir plus, la lecture de mes leçons de logique catégorique.
Je colle ci-dessous (et je commente en même temps) le message reçu d'un membre qui ne peut pas poster dans ce forum:
C'est 'f(a)' qui est appelé 'terme applicatif' et non pas 'f', qui pourrait être appelé 'terme fonctionnel'.Envoyé par Ziploppe
Il ne faut pas penser aux énoncés comme des entités pouvant être vraies. C'est justement la nouveauté introduite par Heyting que de ne considérer que la notion de démonstrabilité, et non pas celle de vérité. A aucun moment je n'ai parlé de 'vrai', j'ai simplement parlé de démonstration. Evidemment, on peut toujours penser que ce qui est démontré est vrai, mais à mon avis ce n'est qu'un facteur de trouble. D'autant plus que la sémantique de Heyting peut s'appliquer aussi bien à la logique classique (dans laquelle les seules valeurs de vérité sont 'vrai' et 'faux') qu'aux logiques non classiques qui ont d'autres valeurs de vérité. Je crois qu'il faut réellement oublier toutes ces notions de 'vrai' et 'faux'. Par ailleurs, un énoncé n'est pas non plus une relation. Il vaut mieux voir un énoncé comme l'ensemble de ses propres preuves. Dans le cas de E => F c'est l'ensemble de toutes les fonctions produisant une preuve de F à partir d'une preuve de E. C'est d'ailleurs comme cela que Heyting s'est exprimé dès 1930.
C'est tout à fait ça. Imaginons qu'on ait à formaliser la notion de preuve dans un logiciel. On serait amené à représenter les preuves de E => F comme des fonctions, justement pour pouvoir mettre ce principe en oeuvre. Précisément, être capable de calculer une preuve de F chaque fois qu'on aura à la fois une preuve 'f' de E => F et une preuve 'a' de E. En appliquant la preuve 'f' de E => F à la preuve 'a' de E, on calcule la preuve 'f(a)' de F. Je crois que ceci exprime bien clairement ce qu'on entend par 'implique'.
Il faut quand même faire attention au vocabulaire. Si E et F sont des ensembles (ou des types), il est clair que toute expression de la forme (x:E) |-> K[x], avec K[x] de type F, représente une fonction de E vers F, c'est à dire une donnée de type E -> F. Maintenant, si E et F sont des énoncés, il vaut mieux pour être précis, introduire l'ensemble des preuves (ou plus exactement des témoins) de E, qu'on pourra noter Proof(E) et faire de même pour F. Dans ces conditions, tout terme de la forme: (xroof(E)) |-> K[x], avec K[x] de type Proof(F), sera lui-même de type Proof(E => F). Maintenant, il est clair qu'il existe éventuellement plusieurs façons d'écrire une preuve pour un énoncé donné. Le principe de l'unicité du témoin dit que toutes ces preuves représentent le même témoin. Il ne dit pas qu'elles s'écrivent toute pareil. De même que deux fonctions écrites différemment peuvent donner les mêmes résultats sur les mêmes données (elles sont alors 'égales').
Les objets ne peuvent pas fournir une bonne analogie, car ils sont par essence non déterministes. Ils sont soumis au principe d'identité (l'un des principes de la POO) qui est en contradiction flagrante avec la notion même d'ensemble. En effet, quelle que soit la classe considérée, tu peux créer autant d'instances que tu veux, et elle sont toutes distinctes, mêmes si elles ont les mêmes attributs. Ceci fait que la notion d'égalité pour les objets est de nature absolument non mathématique, mais plutôt de nature physique. Ceci implique qu'une classe n'est réellement pas un type et encore moins un ensemble. Une classe doit plutôt être vue comme un 'procédé de fabrication de ses propres instances', et les instances elles-mêmes appartiennent définitivement au domaine non déterministe, donc extra-mathématique.
Ceci dit, si dans ce que tu dis je remplace 'classe' par 'ensemble', et 'instance' par 'élément', je suis d'accord avec toi sauf sur deux points:
1. 'f est une méthode pour exprimer une instance de E en instance de F'. Je dirai plustôt: 'f est une méthode pour obtenir un élément de F à partir d'un élément de E (en bref c'est une fonction).
2. '|-> est la classe preuves de E => F dont f est une instance'. Non, |-> n'est surement pas une classe. C'est quelque chose de très méta-mathématique (ou méta-programmatique), c'est juste un concept syntaxique (grammatical) qui donne un moyen d'écrire des termes qui représentent des fonctions.
Je pense que tu as compris le rapprochement entre appliquer une fonction à un argument et utiliser une hypothèse de la forme E => F. Si c'est le cas, c'est déjà bien.
La logique mathématique est une discipline particulièrement troublante et difficile à aborder. Il n'est donc pas étonnant que tu ais quelques difficultés au début. Il faut de toute façon d'abord te débarrasser de l'idée que les énoncés peuvent être vrais ou faux (des notions qui ne font que parasiter la logique, car incompatibles avec le caractère structurel des connecteurs logiques). Il ne faut s'intéresser qu'au fait qu'ils sont démontrables ou non, ce qui n'est pas pareil.
Merci de ta participation.
Je te remercie pour ces informations, et je suis allé voir tes cours qui sont très bien faits, ils me seront très utiles le jour venu !
Je trouve le parallèle maths/informatique saisissant !
Cependant, lorsqu'un analyste ( je ne parle pas de "programmeur" qui a un rôle trop technique pour s'apparenter à un analyste ) analyse et conçoit une application, j'ai l'impression qu'il a un état d'esprit différent que celui d'un mathématicien qui cherche à prouver/démontrer, bien que les similitudes que tu as soulevées soient irréfutables.
Un analyste va examiner les besoins, produire un modèle conceptuel pour y répondre et l'exprimer dans un "langage" ( merise/uml/autre ), ensuite, à partir de son analyse, il va passer à la phase de conception. Une fois l'application developpée, il va la tester et la valider. Je n'ai pas l'impression que dans cette façon de faire, il y ait un souhait de "prouver" ou de "démontrer" que le modèle correspond à la réalité. Les moyens utilisés pour produire le modèle sont des moyens pratiques, comme l'énumération des entités, la génération des Use Case, etc.. Qui ne représentent pas une preuve ou une démonstration.
Il y a de plus différentes façons de résoudre un même problème, et parfois, ce n'est pas la manière la plus "logique" qui est choisi, pour des raisons de contraintes matérielles ou financières par exemple.
Tout cela pour dire que bien que la similitude soit grande, un analyste et un mathématicien ne procèdent pas de la même façon pour "résoudre" un problème, et chaque méthode a ses défauts et qualités, le mieux à mon avis est d'utiliser les deux compétences conjointement pour produire un résultat à la fois pratique et "sûr", mais il faudra des personnes baignées dans les deux mondes, il faudra des informaticiens mélangés à des mathématiciens, et une fois de plus j'insiste sur le fait qu'étant donné que la façon de procédée est différente ( et aussi une question de gout et d'aspiration je pense ) on ne pourra pas faire des informaticiens qui "prouvent" leurs programmes systématiquement, et on ne pourra pas non plus faire des mathématiciens qui utilisent des méthodes pratiques informaticiennes pour démontrer leurs algorithmes..
J'ai l'impression d'être tétu sur ce coup làJe me sens tout petit face à ton parallèlisme preuve/programmation avec mes commentaires !
Je peux apporter ma brique "pratique" à l'édifice
Salut KilVaiDeN, et merci pour le compliment concernant mes leçon de logique. J'espère seulement qu'elles sont lisibles par le plus grand nombre. Ce n'est pas facile, car il y a des notions incompressibles.
Comme tu l'as constaté le parallelisme 'maths/info', ou du moins 'logique/système de types' est saisissant. Il y a vraiment une profonde analogie de structure. Maintenant, cela ne vient pas du tout en contradiction avec ce que tu dis. Dans un projet informatique, pour résoudre un problème réel, les mathématiques ne peuvent pas tout résoudre. Il est bien certain qu'on peut toujours faire des programmes formellement corrects, mais qui en définitive ne font pas ce qu'on voulait. Et là les mathématiques ne peuvent absolument rien. Elles peuvent seulement nous aider à maintenir une certaine forme de cohérence (et donc à éviter certains bugs, mais pas tous). Donc il est bien certain que les mathématiciens ne remplacent pas les développeurs. Ils peuvent seulement aider. Je suis donc bien d'accord avec toi que le mieux est de travailler avec des équipes de gens dont les compétences se complètent. C'est de toute façon beaucoup plus enrichissant.
Mon but dans l'immédiat est seulement de démystifier les mathématiques auprès des développeurs, et d'essayer de faire comprendre qu'on aurait tort de s'en passer en programmation. Elles font peur à certains, mais je crois qu'il n'y a aucune raison valable pour qu'il en soit ainsi. Démontrer n'est pas plus dur que programmer. Moi qui ai beaucoup fait des deux, je peux te le garantir. Ce qui est dur est plutôt de savoir quoi démontrer, de même qu'en programmation le plus dur est de savoir précisément ce qu'on veut que le programme fasse. Une fois qu'on le sait, c'est plutôt facile de developper.
Un projet "secret" que je mène en ce moment, est de faire une documentation sur l'informatique générale.
Je me base sur mon expérience et ma compréhension de la chose pour le faire, et parfois il est vrai qu'il est difficile de compresser le savoir plus qu'on ne le peut de manière à ce qu'il puisse être ingurgité facilement.
Cependant, la pillule passe mieux ( ah ah ) je trouve, en présentant les choses de manière graphique et sonore : par exemple, faire une démonstration en utilisant quelque chose comme wink et en ajoutant un fond sonore ! Il suffit de voir les cours de Vincent Brabant pour s'en rendre compte
J'ai déjà fait plusieurs démos de mon cours (l'introduction, et le début du cours en lui même), et je pense qu'il sera fini courant 2006 ( je n'ai pas de date précise )...
Je pense que tu as raison dans ta démarche : il faut demystifier les mathématiques, beaucoup d'informaticiens ( y compris moi ) y voit une sorte de "bête noire", difficile à appréhender. Mais la manière dont tu le présentes me laisse croire que j'ai peut-être eu tort de penser ça un jour, et je compte bien ( en plus des cours que je prend actuellement ) prendre le temps de réapprendre certaines notions que j'ai laissé de coté et qui pourtant ont un parallèlisme fort avec l'informatique et même une application concrète dans le cas des programmes manipulant des entités mathématiques ( graphique, 3d, audio, etc.. )
Je trouve ça génial qu'un mathématicien s'interesse au monde de l'informatique, aurais-tu donc une "passion" pour l'informatique, qui te pousse à rapprocher ton domaine de prédilection avec ce domaine un peu "chaotique" et où l'on voit beaucoup de choses contradictoires ? Merci encore pour ton aide et ta contribution qui je pense va être de taille dans le monde de l'informatique !
La méthode B est utilisée dans les systèmes embarqués très sécurisés (SIL 3 à 4), de manière quais systématique d'après des discussions que j'ai eues.
Ainsi dans les organes vitaux des trains (Freins), les satellites, pour ouvrir une porte automatique sur un quai de gare (hé oui)...
Malheureusement, souvent pour des raisons de coûts, quand il s'agit de développements non régis par des normes, la preuve de programme est délaissée. Pourtant, les filières informatiques nous apprennent à en faire. Pas de manière aussi poussée et abstraite que dans ce fil bien sûr
Et pour continuer le débat:Merci pour ces précisions. Si j'ai dit 'en particulier dans le train' c'est parce que je savais qu'ils utilisent B pour le train, mais je ne savais pas que c'était exclusif.Deux corrections à apporter à ton discours (d'après ma propre expérience), d'abord, c'est Alstom et non Alsthom (et ce depuis un certain nombre d'années déjà
Et ce effectivement pour une raison de coût.
Maintenant, quand tu dis que c'est 'pour une raison de coût', tu veux bien dire que l'utilisation de B diminue les coûts, ou bien tu veux dire le contraire ? Ce n'est pas clair d'après ta réponse. Ce serait bien de préciser.
Là aussi, il serait intéressant que tu donnes quelques précisions. Je ne connais pas les résultats dont tu parles (je ne suis sans doute pas le seul). En particulier ce serait bien que tu expliques clairement le lien avec l'utilisation du B (ou autre système à preuve) et le coût.Maintenant je ne me lancerai pas dans la comparaison des différents résultats des filiales d'Alstom mais les résultats parlent d'eux mêmes.
Je ne fais pas systématiquement de la preuve de programme, mais j’y fais souvent appel lorsque j’ai un doute.
Un exemple concret : Je travaille dans l’embarqué depuis 3 ans. Quand j’ai débuté dans la PME, je devais reprendre un vieux projet en C.
L’architecture du projet fait qu’il est impossible de tester les modules en unitaire, il faut tester le logiciel sur cible et alors chaque module est en interaction avec les autres.
Pour une demande d’évolution de specs, je devais revoir un algorithme d’une fonction. Je réécris donc l’algorithme par apport aux nouvelles spécifications.
Sachant que je ne pourrais pas tester ma mouture en elle-même, j’en fais une preuve. Tout était correct. Vient ensuite la phase de test. Je commence par le test qui activait forcement mon algo et là...ça ne passe pas.
Je revois donc ma preuve, heureusement simple. Non, pas de doute, ce que j’avais écris était correct, mais pourquoi le test ne passait plus ?
Je me lance donc dans la preuve de l’ancien algo...tient, une erreur bête, le résultat d’une taille est trop grand de 1 (tableaux à base 0 en C). Intrigué, je cherche les endroits où cette fonction est utilisée.
Un programmeur de génie avait trouvé l’erreur de calcul par empirisme je suppose. Il avait décrémenté de 1 le résultat de ladite fonction. Résultat, ces deux fonctions appelées en séquence systématiquement donnaient un résultat juste avec deux algorithmes faux !
Les tests ne suffisent pas à prouver qu’un programme est juste, la preuve est faîte
Bonjour, et merci pour ce fil qui, bien que ardu par certains cotés (on est assez loin des "comment je fait pour debboger mon prg" - fautes incluses) est trés enrichissant.
Ma question : un programme est prouvé par rapport à quoi ? Par rapport à un problème, ou plus exactement par rapport à son énoncé (J'ai bon jusque là ?). Pour avoir un programme prouvable, il est donc essentiel que son énoncé soit défini de façon claire et sans erreur d'interprétation possible. On se rapproche donc d'une définition mathématique (dans le sens "avec un langage ne permettant pas l'ambigüité") du problème à résoudre.
La méthode Z permet (si ma mémoire est bonne) d'analyser correctement un énoncé, mais n'y a-t-il pas ici un travail méthodologique à faire ?
Par ailleurs, je ne crois pas qu'il faille opposer "preuve" et "test". Si je monte dans un avion, et que j'entend l'hotesse annoncer "ceci est le tout premier vol de l'appareil. Il n'a jamais été testé, mais il a été prouvé que tout va bien se passer", j'aurai une furieuse envie de redescendre...
Enfin, n'a-t-on pas ici deux cas de figures :
- les informaticiens de gestions, dont le pb principal est de comprendre ce que veut l'utilisateur/client (et bien souvent de faire en sorte que l'utilisateur/client sache ce qu'il veut, hormis une baguette magique pour faire le travail à sa place)
- les informaticiens industriels, qui au moindre bug vont voir la ligne de production s'arréter (coût : 10000euros/heure) ou la rame de la ligne 14 s'encastrer dans un mur (coût : qques millions d'euros, et accessoirement une vingtaine de vies humaines)
Les besoins et les coûts ne sont pas du tout les mêmes dans les deux cas. J'ai passé récemment une échographie, et le médecin -ayant appris que j'étais informaticien- m'a dit en me montrant l'appareil "ça, ce n'est pas comme windows, ça ne plante pas". Ce à quoi je lui ai répondu "seriez vous prêt à payer un ordinateur faisant uniquement du traitement de texte au prix ou vous avez acheté cette machine ?"
Une solution n'est valable que dans un contexte donné.
Mais ce n'est pas une raison pour que les deux mondes s'ignorent (voire se méprisent), et c'est la raison de mon intérêt pour ce topic.
Yvan
La preuve de programme est essentielle pour des projets volumineux.
Immaginons un projet de 800 000 lignes dans divers langages (c++, delphi, autre).
Il est facile d'immaginer que ce projet prend un temps conséquent à être validé voir qualifié. Allez soyons optimistes, une année.
Et que pour des raisons de turn over des programmeurs, tout n'est pas tout à fait modulaire.
Arrivé à 6 mois de validations réussies, la catastrophe: UN bug qui remet en cause un module largement ré-utilisé.
6 mois de Validation à reprendre après débug.
Une preuve de programme globale serait bien sûr trop coûteuse. Mais pour certaines parties, ça évitera de voir le bug trop tard.
Prouver un programme c'est montrer qu'il est confoirme au traitement attendu.
Il y a forcément un moment où il faut faire des hypothèses non prouvables mathématiquement, car les mathématiques n'apportent des certitudes que sur les mathématiques elles-mêmes. Par exemple, pour un projet industriel, il faudra faire des hypothèses sur la fiabilité de tel ou tel organe. Ceci dit, le simple fait de se poser ces question peut amener à concevoir des améliorations de ces organes ou des procédures de secours. Par exemple, on pourra formaliser des évènements comme 'l'organe ne fonctionne plus', et en tenir compte dans ce qu'on veut prouver.
La formalisation est correcte, mais la question est de savoir si la sémantique formelle de cet énoncé correspond à la réalité. Encore une fois (j'ai peur de me répéter, mais je ne me souviens pas de tout ce que j'ai écrit dans ce fil), la preuve n'est pas tout. Ce n'est qu'un outil parmi d'autres pour faire de bons logiciels. Il n'y a donc pas à mon avis lieu qu'il y ait querelle entre deux mondes. Il y a de toute façon un travail méthodologique (extra-mathématique) à faire. C'est un truc bien connu d'ailleurs des sociétés qui font du système expert. Pour faire un système expert, il faut un programmeur et un expert. Ce sont rarement les mêmes personnes.
donc aussi pour des petits modules qui seront intégrés dans des projets volumineux.
sans doute beaucoup moins si on a pris soin de prouver les modules au fur et à mesure de leur développement. Mais prouver est plus ou moins difficile suivant le caractère plus ou moins impératif du langage. Les langages très impératifs découragent la preuve assez clairement. Ils ont aussi l'inconvénient en cas de manipulation de variable globale dans tout le projet de rendre la modularisation de la preuve éventuellement impossible.
Ca c'est un gros problème, mais je crois qu'il est plus methodologique que technique. Sur ce point l'eXtrem Programming peut sans doute aider.
En fait la preuve doit être modulaire comme le programme lui-même. La question me semble-t-il est surtout de ne pas penser qu'on va prouver le programme une fois qu'il sera fini. Il faut que l'activité de preuve soit menée en parallèle avec le développement Elle doit en faire partie intégrante. C'est ce à quoi oblige le système B par exemple.
La difficulté est de formaliser ce qu'on veut qu'il fasse. C'est souvent plus difficile que de prouver. Voir plus haut ma réponse à ypicot.
As-tu une expérience de preuve ou de tentative de preuve de programme dans ton entreprise ?
Bonjour
J'ai un peu de mal a suivre les interventions vu que je ne suis pas de formation informaticien, ni mathématicien, ni même astrophysicien
Je vois bien evidemment les intérets d'un systeme de preuve. Et de ce que j'ai pu en lire, la preuve c'est constitue par:
Des facteurs ambients:
Les commentaires du code, l'oeuil du developpeur, la qualité de l'environnement de développement, les fonctionnalités du language...
L'utilisation de normes, methodes et conventions:
La qualité des commentaires, la qualité du developpement, la qualité de la modélisation...
Des outils pratiques et concrets:
Logiciels dedies aux preuves
DrTopos, je ne suis pas d'accord avec vous sur ce point. Notre etat d'avancement actuel ne peut nous permettre de faire confiance qu'a nos simulations theoriques. Les tests grandeur nature, dans des conditions d'exploitation normale, voire extreme permettent justement de valider nos preuves.Ce que tu proposes s'apparente à la notion de test, pas de preuve. Car c'est seulement à l'exécution qu'on va savoir que y est nul, pas à la compilation. Ce n'est pas le même genre de prévention. Je fais une comparaison extrème (et un peu caricaturale, j'en conviens) avec l'automobile. Est-ce que le constructeur doit se préoccuper de faire des freins qui ne lacheront pas, ou est-ce qu'il peut se contenter de donner un numéro de téléphone auquel lancer une exception après que les freins auront laché ? C'est là toute la différence.
N'utilise-t-on pas des vraies vehicules avec des mannequins dedans pour etudier la deformation d'une structure? les protoypes de plaquettes de frein ne sont elles pas testees sur des vraies roues en laboratoire?
Je suis d'accord que les preuves ont une place, j'utilise un système semblable, mais a mon avis, sans les tests cela reste que du théorique inutilisable tel quel en pratique.
Donc en pratique, pour la preuve:
- Oui il faut une excellente gestion des exceptions
- Oui il faut des tests unitaires
- Oui il faut des fuzzers
Pas pour qu'ils s'executent chez le client final, mais qu'ils se produisent dans votre labo.
Continuons dans le pratique, et voyons l'etat des choses aujour d'hui:
- On a les outils
- On a les methodes
- On a l'ambiance
Or dans le meilleur des cas, les sytemes de validation sont largement sous exploités, limités aux naifs tests unitaires. S'ils sont très élabores et très chers, je suis persuadé qu'ils restent incomplets. Les outils n'interragissent pas, les methodes sont difficiles a mettre en oeuvre simultanement et n'ont pas de dynamique commune. Il n'y a pas de cohérence de fond, c'est le Moyen-Age.
Comment mettre en place un systeme de validation exploitable naturellement, intuitivement et efficacement aujourd'hui?
Il faut donner une grammaire a l'application, mais:
- Bien sur les Mathematiques sont le squelette de toute chose, mais cette grammaire ne prend pas comme point de départ les mathématiques.
- Le logiciel doit produire des nouvelles phrases vérifiable par la grammaire de base
- Cette grammaire doit être commune a l'application mais aussi aux outlis qui la testent, les tests ne sont plus seulement unitaires
En pratique:
- Gérer plusieurs compilations d'une meme application dans des buts particuliers en preservant les fonctionnalités demandées (et ca va bien au delà du simple "DEBUG")
- Travailler sur l'automatisation de la création de l'environnement d'éxecution de l'application, et sur l'automatisation de l'interprétation de cet environnement apres l'execution ciblée de certaines fonctions de l'application
- Donner aux lignes de log une signification plus qu'informative (idéalement: l'application est en mesure de "rejouer" le log)
...
Fin de ma petite parenthese
Je viens de découvrir Anubis
C'est exactement ce que je me suis dis apres m'être posé la question suivante:Pour la première fois, les objets mathématiques, au lieu d'être définis par des constructions ensemblistes, étaient définis par une description de leur comportement global vis-à-vis des autres objets mathématiques
"Comment un matheux en serait arrivé a se poser des questions sur le systeme de preuves?"
Je vais essayer de comprendre un peu plus ce que vous avez fait pour voir le rapport avec ce que j'ai fait
Il me semble que le test et la preuve sont deux choses distinctes.
Le test, c'est dire en gros "on n'a trouvé aucun cas où ça ne marche pas"
La preuve, c'est dire "il n'existe aucun cas où ça ne marche pas".
Prenons par exemple le théorème de Fermat.
Depuis le 17ème siècle, les mathématiciens se sont évertués à prouver que ce théorème était juste. Des tas d'ordinateurs ont tourné pour essayer de trouver un contre-exemple, sans succès.
On a donc testé le théorème, mais on ne l'avais jamais démontré (ou prouvé). Ce n'est que récemment (1994, merci google) qu'il a été démontré.
Yvan
C'est tout à fait certain, mais ce n'est pas forcément évident pour tous. Je pense que ce fil a justement aidé à faire la différence.
Exact, même s'il y a une infinité de cas.
Du point de vue du programmeur, je crois que l'argument le plus frappant pour distinguer un test d'une preuve, est le fait que le test agit à l'exécution, alors que la preuve agit au moment de la compilation. C'est une façon de satisfaire le proverbe 'Il vaut mieux prévenir que guérir'. L'autre inconvénient du test (comme il ne saurait en général être exhaustif) est qu'il n'apporte pas la certitude formelle que le problème testé n'existe pas.
Ceci dit, le test reste d'actualité pour tout ce qu'on ne peut pas démontrer (essentiellement parce qu'on ne sait pas comment le formaliser). Pour être plus concrêt, je donne un exemple: le problème de la division par zéro relève de la preuve, alors que l'adéquation du soft (même formellement correct) au business réel du client relève du test, du moins tant que ces besoins ne sont pas formalisés. Par exemple, un logiciel peut être 'parfait' et cependant inutilisable par un mal voyant. Il est clair que les mathématiques ont une portée limitée sur ce genre de problème.
Je pense au contraire qu'on est parfaitement d'accord, mais il semble y avoir une confusion entre preuve et spécification. Une spécification est un énoncé qu'il est possible de prouver, et il n'y a aucune raison de mettre en doute la validité de la preuve si elle est faite avec de bons outils. Par contre, l'adéquation de la spécification à la réalité est autre chose, et c'est cela effectivement qu'il est indispensable de tester. Encore une fois, les mathématiques ne démontrent jamais rien quant-à la réalité physique de notre monde. Il reste toujours le problème de la modélisation du réel, qu'on utilise à cette fin des mathématiques on non.
Tout à fait d'accord, et ça confirme ce que je viens de dire plus haut.
Non pas d'accord, pour la preuve il faut un mathématicien ou quelqu'un capable d'écrire une preuve correcte éventuellement avec l'aide d'un système de formalisation des preuves.
Quant-aux exceptions, on en a déjà discuté ci-dessus. Pour moi, c'est un faux problème. D'ailleurs en Anubis, cette notion n'existe pas.
Je dirai même que c'est l'âge de pierre, en plus d'être la tour de Babel. En mathématiques, tout le monde utilise un seul et unique langage, et ce depuis des siècles. On peut quand même avoir l'espoir qu'en informatique on arrivera un jour à quelquechose de similaire.
Par ailleurs, une validation par test n'a pas valeur de preuve. J'en reviens aux arguments déjà donnés: la division par zéro doit être évitée par preuve. Cette question n'a rien à voir avec des tests.
Je n'irai pas jusque là. Mais il est certain que leur universalité a fait ses preuves.
Les problèmes que tu évoques avec les systèmes de tests me semblent plus venir du manque de maturité de ces systèmes ou même du fait qu'on veut les appliquer à des programmes écrits dans des langages pas du tout conçus pour cela. Je crois que si on veut des systèmes de preuves facilement utilisables et efficaces (et pas chers), la première chose à faire est de changer les langages de programmation.
Je suppose que tu évoques ici les langages fonctionnels, qui -d'après ce que j'ai compris- sont beaucoup plus simples à "prouver" (notamment pour la terminaison, par exemple en utilisant des fonctions récursives)
Mais est-il suffisant de dire qu'un langage est fonctionnel pour que tout à coup tout soit prouvable ? Je pense entre autre à OCaml (dsl, je n'ai pas encore eu le temps de mettre le nez dans Anubis), qui est à la base un langage fonctionnel (Caml), mis à la sauce objet (O). En programmant en OCaml, j'ai toujours eu l'impression de mettre de coté l'aspect fonctionnel, et tous ses "bénéfices" (qui n'ont d'ailleurs jamais été clairs pour moi).
Yvan
Je crois qu'on a tort d'opposer 'fonctionel' à 'impératif'. Il me semble que le contraire d'impératif serait plutôt 'déterministe' (absence d'effet de bord). Le fonctionel en soit n'est qu'un moyen de favoriser le déterminisme.
Le bénéfice du déterminisme est qu'on a une sémantique des programmes beaucoup plus facile à comprendre. En effet, aucun symbole ne change de valeur dynamiquement, et le sens du programme ne dépend de l'état d'aucune variable. Mon expérience me confirme très clairement que le non déterminisme est la source de bugs numéro 1.
Maintenant, les objets de la POO, de par leur nature concrête sont essentiellement non déterministes. Il est clair qu'on ne peut pas se passer d'objets. On pouvait le faire du temps où les programmes faisaient du calcul pur, mais maintenant qu'ils sont interactifs, ce n'est plus possible. Toutefois, je crois que c'est une énorme erreur de faire du 'tout objet', car on rend tout de facto non déterministe. Les objets sont utiles, mais ils ne doivent pas envahir toute la programmation.
Dans le manuel d'Anubis, j'ai développé un peu plus ces idées.
Bonsoir,
Merci de vos explications ypicot et DrTopos. Je n'avais absolument saisi cette distinction tout en étant en total accord avec vous DrTopos sur vos explications dans l'aide d'Anubis (abandon de certains aspects de l'Objet, utilisation fondamentale de la recursivité etc...)
J'ai crée un systeme fonctionnant uniquement avec des metadonnées qui permettent entre autre, de créer un ensemble de règles concernant une donnée, mais aussi de gérer toutes les formules dans laquelle cette donnée intervient, ainsi que toute la gestion des décisions a prendre en conséquence. L'application se contente d'appliquer.
Il m'a fallu une semaine pour peniblement reussir a comprendre les principes de fonctionnement d'Anubis, qui pourtant est simple.
Le fait de tenter d'appliquer dans l'idee votre demarche a ce que j'ai cree, m'a permi de decouvrir deux de mes defaillances:
- Le systeme que j'ai fait n'est pas efficace compare au votre, puisque je me basais uniquement sur des tests (j'avais pas pense a faire des demonstrations mathematiques sur les formules)
- Poussant le raisonnement un peu plus loin sur l'origine de mon erreur, considérant votre raisonnement par rapport au mien, et qu'en regle générale, nos travaux sont le fruit et l'empreinte de notre reflexion, j'ai en même temps découvert que je suis dyslexique
Ne serait-ce pas la un debut de "Preuve" que votre demarche est la bonne et que les Mathematiques seraient bien le squelette de toute chose?
Apres plusieurs recherches, j'ai pu mettre des concepts nommés sur ce que je fais et sur la maniere dont je considere la preuve.
Le système fonctionne sur la base de meta données
Il s'agit en fait d'un système ontologique, dans lequel tout est consideré comme prouvé. La mecanique de preuve se déroule en deux phases: le systeme valide une grammaire spécifique par un systeme de reglès, la véracite de l'ensemble de ces règles étant prouvée au préalable par un prouveur de theorèmes automatisé (ca c'est ce qu'il me reste a faire).
Soit le système est utilise tel quel, c'est a dire en utilisant sa grammaire (on ajoute des metadonnées). Soit ses capacites sont étendues (on ajoute des interpreteurs de metadonnee), ce qui implique une re-validation partielle pour les nouveaux élements de la grammaire.
Salut Piotrek.
Ce que tu fais a l'air très intéressant. Toutefois, tes explications n'en donnent pas une idée très précise. Qu'entends tu par valider une grammaire? Par exemple, YACC valide d'une certaine façon une grammaire en assurant qu'elle est exempte d'ambiguïté. Je suppose que dans ton projet, il s'agit de quelquechose de plus sophistiqué. De plus de quel genre de grammaire s'agit-il (LALR, etc...)? Ou bien ta grammaire est-elle une sorte de programme PROLOG (c'est-à-dire un ensemble totalement ordonné de clauses de Horn)?
Je suppose que tu entends par méta-données des données qui vont servir à générer des programmes. Est-ce bien cela ?
Il y a une chose que je crois bien comprendre malgré tout dans ce que tu dis. C'est le fait que tout système (programme exécutable) sensé prouver quelque chose doit être lui-même préalablement prouvé, même si en dernière analyse, et en remontant à la source, le premier de ces systèmes doit forcément être prouvé à la main.
Ce serait intéressant que tu expliques un peu plus de quoi il s'agit, en particulier en expliquant les termes que tu emploies. (J'ai visité les deux pages de Wikipedia que tu cites; elles restent elles-mêmes assez floues sur les concepts qu'elles sont sensées définir.)
Vous avez un bloqueur de publicités installé.
Le Club Developpez.com n'affiche que des publicités IT, discrètes et non intrusives.
Afin que nous puissions continuer à vous fournir gratuitement du contenu de qualité, merci de nous soutenir en désactivant votre bloqueur de publicités sur Developpez.com.
Répondre avec citation
Partager