Discussion :

[Matthieu Brucher]

On a eu hier un petit séminaire sur la preuve formelle de la racine carrée de GMP sous Coq. Apparemment, c'est la première fois qu'une démonstration assez complète a été faite, pas seulement de l'algorithme, mais du code C aussi et avec vérification des overflow, de la mémoire, ...
Ils ont mis 1 an et demi, mais pas à plein temps, l'outil qu'ils ont utilisé était développé en même temps, pour 20 lignes de code.
Le gars estime à 2-3 mois le temps qu'il faudrait maintenant, mais il y a des tonnes de contraintes à définir au fur et à mesure, même avec l'outil assistant.
Je pensais que ce serait simple de démontrer quelque chose, mais là, j'ai eu peur ! Si tout le monde devait faire ça

[DrTopos]

C'est quoi GMP ? Un logiciel de calcul formel ? Pourrais-tu donner plus de précisions sur ce qui a été prouvé précisément. Merci.

[Matthieu Brucher]

C'est la GNU Multiple Precision Arithmetic Library.
La démonstration a été faite que la fonction racine carrée utilisée était valable algorithmiquement et que le code lui aussi était valide, à savoir que la racine carrée se fait sur place, donc il a fallu démontrer que ça marchait effetivement. La preuve est ici : ftp://ftp-sop.inria.fr/lemme/Nicolas.Magaud/GMP-sqrt-why/index.html

[DrTopos]

Bonjour à tous.

Je viens de parcourir l'article cité par Miles:

ftp://ftp-sop.inria.fr/lemme/Nicolas.Magaud/GMP-sqrt-why/index.html

C'est sûr, ça fait peur. Mais c'est pour une grande part dû au fait que les auteurs essayent de prouver des programmes écrits en C. Comme le C est des plus laxistes sur les question de sûreté, il est clair qu'ils se sont placés dans le pire des cas. Par exemple, avec un langage bien ficelé sur le plan logique, il n'y aurait aucun besoin de faire une preuve qu'il n'y a pas de dépassement de capacité. Je dirai même qu'à la limite, la preuve que l'algorithme mathématique utilisé pour la division est correct devrait suffire. Par exemple, si on écrit un programme en Anubis (ou avec quelques autres langages dits de 'haut niveau'), de telles choses n'ont pas à être prouvées. Le dépassement de capacité est impossible quelle que soit la façon de programmer.

Alors, évidemment, il y a quand-même une 'fausse bonne' raison d'utiliser le C: les performances. C'est clairement une bonne raison. Il est bien entendu inutile de convaincre qui que ce soit que dans certaines applications des performances optimales sont requises. Et donc, la question est de savoir si le fait d'utiliser des langages logiquement sûrs (de haut niveau, comme Lisp, CAML ou Anubis) est incompatible avec des performances élevées, et si cet état de fait est ou n'est pas une fatalité.

Lisp CAML et Anubis (surtout Anubis d'ailleurs, je ne le cache pas, mais Anubis doit être considéré comme un prototype dans son état actuel) n'ont pas les performances du C à l'exécution. Toutefois mon opinion reste que ce n'est pas une fatalité, mais qu'on ne peut arriver à concilier haut niveau (sûreté) et performances optimales que si le langage de programmation permet d'écrire des énoncés mathématiques (des vrais énoncés, pas des expresssions à valeurs booléennes) et des preuves. J'ai déjà développé ce point de vue ici avec pas mal de détails:

http://www.developpez.net/forums/vie...208624#2208624

Moralité: ne pas se laisser abuser par cet exemple, que je ne considère pas comme significatif, surtout au regard de ce qui se prépare pour l'avenir. Je crois que c'est surtout un exercice de style. Donc je maintiens: il ne faut pas avoir peur des preuves.

[KiLVaiDeN]

Salut tout le monde, de retour sur ce thread car il est remonté en tête des threads actifs auquels j'ai participé.

J'ai également jetté un oeil à l'article cité : je trouve que la complexité de celui-ci est rebutante, et qu'un informaticien ne devrait pas avoir à se "mouiller" dans un travail de "mathématicien".

Je ne sais pas si c'est dû à mon incompétence en la matière (maths), mais finalement ne faut-il pas donner les bons rôles à chacuns ? Un informaticien n'est pas là pour faire des preuves mathématiques : il manipule des concepts de haut niveau, et fait un travail concret et utile. Un mathématicien quand à lui, étudie les fondements, et fournis à la rigueur les outils que l'informaticien peut alors utiliser pour batir ses applications.

Ceci est la remarque du jour, vos avis sur ce sujet sont les bienvenues !

Par ailleurs, j'ai une question pour MrTopos : Il est vrai que le C n'est pas adapté de base à la preuve d'un programme. Cependant, ne serait-il pas possible, au lieu de developper un nouveau langage, d'agrémenter le C existant de fonctions "prouvées", et d'objets "prouvés", dont l'utilisation constante suffirait à produire un programme à son tour "prouvé" ?

Il est vrai qu'on ne peut pas interdire à un programmeur C d'utiliser un pointeur par exemple. Mais on peut l'inciter à utiliser des fonctions de la librairie "prouvée" si il a besoin d'une fonctionnalité sûre dans son programme.

Ce mécanisme pourrait donc permettre à tous les programmeurs C, d'avoir en plus des outils courants qu'ils utilisent, une librairie "prouvée" utile pour les cas qui le necessitent ( comme ceux que tu as cités, la rame automatique de la ligne 14 par exemple ). De plus, en travaillant en profondeur cette librairie ( et c'est là que le rôle d'un mathématicien intervient à mon avis ) tu pourrais l'optimiser grâce aux possibilités du C.

Je pense à tout ça, car il est vrai que depuis que j'ai commencé à programmer, un de mes soucis majeur a été l'optimisation. Je pense que dans la plupart des taches, le facteur réactivité du programme est crucial pour juger de sa "qualité", en tout cas aux yeux des utilisateurs. L'idée de programmer dans un environnement peu performant ne me motive donc pas trop.. Mais peut-être est-ce stupide comme réaction ? Un souci plus de "hacker" que de vrai informaticien digne de ce nom, qui chercherait plutot à se focaliser sur la vrai qualité du code, et la robustesse de son programme

[DrTopos]

Heureux de te retrouver sur ce fil KilVaiDeN.

Je ne crois pas qu'il faille faire une telle dichotomie entre informaticien et mathématicien. Le fait pour les informaticiens de ne pas vouloir se 'mouiller' (comme tu dis), pour ne pas dire se 'salir les mains' en faisant des mathématiques, de même d'ailleurs que la répugnance bien connue d'un grand nombre de mathématiciens vis à vis de la programmation, relève plus du tabou que d'une nécessité. Il y a de nombreux points communs entre programmation et démonstration (je l'ai déjà dit dans ce fil, mais je n'ai pas beaucoup développé ce point jusqu'à maintenant), et je crois que l'avenir est à ceux qui sauront faire les deux. Evidemment, l'enseignement des maths étant ce qu'il est, beaucoup sont dégoutés très jeunes et ça laisse des traces. C'est vraiment dommage.

Ta suggestion d'avoir une base d'outils prouvés est d'une certaine manière orthogonale au problème de la preuve de programme. On peut considérer par exemple que quand on inclus une bibliothèque C éprouvée (à défaut d'être prouvée) dans un développement en C, on n'a pas à se faire de soucis et on peut faire confiance aux programmes de la bibliothèque. En fait, même en supposant que ce soit vrai, il reste que la façon même de s'interfacer avec la bibliothèque peut introduire des bugs. En fait la preuve de programme est un problème global. On ne peut pas prouver à moitié. Un énoncé (ou un programme) qui est prouvé à 99,9 pour100 n'est pas prouvé. Le bug catastrophique peut se trouver dans le millième non prouvé.

[KiLVaiDeN]

Salut DrTopos, merci pour ta réponse !

Je pense que tu as en effet raison par rapport à la dualité maths/info, un "bon informaticien" digne de ce nom devrait aussi avoir un bagage suffisant en mathématiques pour s'en sortir dans toutes les situations de son métier. Pour ma part, je prend des cours du soir au CNAM pour combler cette lacune Tu dois connaitre Mr Dazy ou Mr Dewez d'ailleurs !

Cependant, j'ai l'impression qu'il est difficile d'allouer une place aux mathématiques dans le métier d'informaticien de nos jours, quand on voit le nombre incalculable de projets informatiques liés à "l'informatique de gestion", et donc ne nécessitant aucune connaissance en mathématiques, même de niveau secondaire.

Faire une application fenêtrée comme par exemple un outil de gestion, faire des requêtes sql, faire de la programmation par objets, utiliser des librairies externes, concevoir des algorithmes liés à une règle métier, générer une analyse en merise ou UML, compiler un programme, apprendre plusieurs langages, comprendre une architecture informatique, connaitre ce qu'est un réseau, voire même connaitre le fonctionnement interne d'un ordinateur, comprendre du code assembleur : tout ça représente la plus grande partie du métier d'un informaticien de nos jours, même niveau ingénieur, et j'ai l'impression que les mathématiques ne sont pas très présentes dans ce schéma. Je mens : la logique est omniprésente, mais en général, soit on a un esprit logique, soit on en a pas, et donc c'est quelque chose presque "d'inée".

Tout ça parce qu'il y a des gens qui préfèrent ce coté de l'informatique : le coté "pratique" de celle-ci, celui qui permet de se servir d'un programme comme d'une solution pour résoudre un problème, même partiellement ! Même si ce programme est mal fait, et qu'il plante 3 fois par semaine, tant qu'il aide au quotidien, il sera apprécié !

J'ai connu le cas de beaucoup d'applications mal déployées, ou bien tout simplement mal conçues, et même des serveurs d'applications peu robustes, qu'il faut rebooter tous les 3 jours : et les gens acceptent le principe du plantage! il y a des domaines ou c'est innacceptable, mais ( merci microsoft? ) le plantage est monnaie courrante, l'essentiel est d'être réactif dans le redemarrage! Des entreprises investissent énormément d'argent pour un circuit de maintenance à base de ticket d'incident, au lieu de résoudre les problèmes récurrents !

Je trouve ça dommage, mais c'est une réalité, difficile à changer, à moins que les gens prennent conscience qu'un vrai programme ou système ne devrait _jamais_ planter, alors ce jour là ce sera différent Peut-être bientot ? Et peut-être grace à toi MrTopos !

[DrTopos]

Je crois qu'il y a essentiellement deux façons d'utiliser des maths en info:

1. On a besoin de modéliser avec des maths un problème qui n'est pas de nature informatique, mais qu'on va traiter avec de l'informatique. Par exemple, si on fait de la 3D, et on a besoin d'algèbre linéaire et de géométrie, ou si on fait de la simulation de système physique, et on a besoin de maîtriser un peu les équations différentielles et les intégrales, ou si on doit mettre en place un automate, avec des changements d'état, on a besoin de maîtriser les questions de causalité et/ou de protocole et ça c'est plutôt de la logique, etc...

2. On a besoin de maths pour modéliser un problème de nature informatique. Dans ce cas, les maths utilisées sont presque toujours de la logique. Par exemple, pour faire un compilateur Prolog ou un optimiseur de requêtes pour SQL, on a besoin de maîtriser le calcul des prédicats, et pour faire le design d'un langage de programmation avec preuves, on a besoin de connaitre de la théorie de la démonstration, etc... Evidemment, ce sont des cas assez rares.

Mais il est vrai que la plupart du temps, dans les applications de gestion on n'a besoin ni de 1. ni de 2, si ce nest qu'un système de gestion est quand même un automate avec des états, et que là aussi on peut avoir des problèmes de causalité et/ou de protocole. Mais en général, ce genre de problème relève du simple bon sens, plus que de la logique proprement dite.

Mais en fait, la question à laquelle je pensais quand j'ai initié ce fil est plutôt de discuter des moyens d'assurer la cohérence globale dans un projet de programmation. Même si un tel projet consiste à 'brancher' des modules tout faits (et déjà 'prouvés') les uns sur les autres, comme tu le suggères, il sagit quand même de programmation à mon avis. La programmation traditionnelle ne consiste-t-elle pas à 'brancher' des expressions du langage les unes sur les autres. Pour que de tels branchements soient corrects (cohérents), il faut que les 'prises' (les interfaces) aient des types aussi fins que possible, c'est à dire qu'on ait des contraintes aussi fortes que possible sur la façon de brancher. En fait la seule différence entre C et un langage à preuves est la nature du système de types, c'est à dire la nature des contraintes de branchements. Mais fondamentalement, c'est le même principe.

C'est vrai quand même ce que tu dis: que ceux qui ne veulent pas trop approfondir devraient se limiter à utiliser des modules 'prouvés', car cette partie de la 'programmation', qui consiste seulement à assembler des modules de haut niveau est sans doute moins complexe que la fabrication des modules eux-mêmes, même si fondamentalement elle est de même nature.

Dans le système que je suis en train de préparer (Anubis 2), les énoncés et les preuves ne sont que des épiphénomènes du système de typage. C'est le fait qu'il y a de nouveaux types (inhabituels, il est vrai) qui introduit ces nouveaux concepts. Et la façon de manipuler les données de ces types ne diffère fondamentalement pas de la façon de manipuler les structures, les tableaux, les fonctions, etc... C'est surtout le vocabulaire qui change. Ce que je veux dire (et qui est d'ailleurs bien connu) est que prouver et programmer sont deux activités tellement voisines que personne ne devrait être gèné pour passer de l'une à l'autre. Ce que j'espère justement c'est qu'Anubis 2 va rendre les deux choses pratiquement indiscernables l'une de l'autre, ou du moins tellement imbriquées l'une dans l'autre qu'il ne s'agira plus que d'une seule activité.

Dans les prochains jours, je vais mettre un post contenant une comparaison précise, point par point entre les principes fondamentaux de la programmation et les principes fondamentaux de démonstration, pour qu'on voit bien le parallèle (et aussi les différences, mais on sera surpris de constater que la programmation est plutôt plus complexe que la démonstration, car elle fait intervenir des notions qui n'existent pas pour les preuves).

[KiLVaiDeN]

Pour argumenter un peu plus, je pense à quelque chose, imaginons qu'un jour prochain ( qui sait peut-être plus tôt qu'on ne le croit ) on réussise à produire une "machine" capable de prendre des décisions ( de faire un choix ). Parfois, et peut-être pour sauver des vies, il faudra non seulement que cette "machine" puisse "traiter les informations" rapidement, mais en plus que son comportement soit "prouvé", car comme tu l'as dit, un système ayant une responsabilité cruciale DOIT être prouvé, je pense que ce serait un projet irresponsable autrement.

Prenons l'exemple d'un robot chargé de sauver des vies en bougeant les débris suite à un séisme important, par exemple, on pourrait imaginer un robot qui fonctionnerait sans intervention humaine.

Pour "programmer" ce robot, en tant que "chef de projet", je pense que l'orientation la plus valable est de mélanger les compétences, de prendre un ensemble de mathématiciens, de mécaniciens et d'informaticiens, voués à travailler conjointement pour développer ce robot. Diviser pour rêgner, diviser pour mieux comprendre, c'est là que les efforts doivent être concentrés, faire un hybride "informaticien/mathématicien" pourrait alors avoir un sens : la personne chargée de faire communiquer un mathématicien avec un informaticien ! Une autre sorte de métier peut-être...

Mais il ne faut pas oublier la complexité des métiers, l'informatique est vaste, les mathématiques également, ce sont des "sciences" à part entière quelque part, et l'époque des savants comme Pascal ou De Vinci est révolue, car il est même impossible de connaitre même un seul de ces domaines à fond je pense.. Donc cette personne "hybride" devrait "se contenter" personnellement de ne maitriser les sciences "qu'à moitié" et quelque part ça peut être réducteur, sans parler du fait que chacun a des préférences...

Je m'éloigne vraiment du sujet là je crois ! Mais ça fait plaisir de discuter avec des gens aussi "callés" et qui n'hésitent pas à donner leur avis, sans avoir la grosse tête, vraiment chapeau !

[DrTopos]

Mais il ne faut pas oublier la complexité des métiers, l'informatique est vaste, les mathématiques également, ce sont des "sciences" à part entière quelque part, [...]

Il est sûr que les métiers sont d'une complexité redoutable, et que pour le mathématicien, les mathématiques paraissent simples à coté de certains métiers. La difficulté d'appliquer les maths à des problèmes réels consiste à modéliser les problèmes. J'ai eu l'occasion de rencontrer des ingénieurs dans des industries de pointe, et on voit bien que l'essentiel du travail à faire pour faire entrer des maths (donc de la sûreté) dans un problème, n'est pas de prouver, mais bien de savoir quoi prouver. C'est donc l'établissement du modèle (des spécifications) qui constitue le vrai défi (qu'on m'excuse de me répéter, j'ai dû déjà dire cela plusieurs fois). Donc en fait, je crois que les ingénieurs et les développeurs auront surtout à manier des énoncés (c'est à dire à comprendre le sens de 'et', 'ou', 'implique', ,quel que soit', 'il existe') plutôt qu'à faire les preuves elles-mêmes. D'ailleurs, une fois les spécification écrites, les matheux se feront un plaisir de les prouver sans embêter personne. De plus, dans le cas des problèmes réels, beaucoup de preuves peuvent être trouvées par les ordinateurs (80 pour 100 d'entre elles dans le cas du logiciel du métro 14). Donc en fait c'est la notion d'énoncé qui doit rentrer dans les moeurs plutôt que celle de preuve. Je suis persuadé qu'on y parviendra, mais pour le moment, l'outil (le langage de programmation, suffisamment attractif, intuitif et simple d'utilisation) manque encore.

[KiLVaiDeN]

Il faudrait donc passer par une étape supplémentaire ?

Par exemple :

Expressions des besoins
=>
Enoncé "mathématique" du(des) problème(s)
=>
Démonstration et preuve (par un mathématicien?)
=>
Elaboration des algorithmes "prouvés" (par un informaticien?)

à voir

[Matthieu Brucher]

Dans mon domaine, c'est purement de la modélisation. Notre plus gros problème est de mettre un modèle adéquat sur nos données avec des hypothèses pas trop foireuses pour que ça tienne la route. Malheureusement, on est pas encore au niveau d'un médecin, même si lui-même n'arriverait pas à faire tout ce qu'on peut faire.
En traitement du signal de manière générale, on doit décrire par un modèle nos données pour en retirer l'information pertinente qui elle-même doit être modélisée. Mais pour prouver que nos modèles sont valides, à part connaitre dès le départ le modèle selon lequel les données ont été générées, c'est statistiquement limite.

[xave]

Mais il y a une contre-partie car on économise beaucoup de debogage, ce qui fait que le coût est à mon avis moins élévé qu'avec les méthodes traditionnelles. Ces méthodes sont appliquées depuis pas mal d'années chez Alsthom, en particulier dans le train. Tout cela pour dire que je ne crois pas à l'argument ``coût''.

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à ), ensuite, ce n'est pas en particulier dans le train que sont utilisées ces méthodes mais exclusivement...
Et ce effectivement pour une raison de 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.

[DrTopos]

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à ), ensuite, ce n'est pas en particulier dans le train que sont utilisées ces méthodes mais exclusivement...
Et ce effectivement pour une raison de coût.

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.

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.

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.

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.

[DrTopos]

Expressions des besoins
=>
Enoncé "mathématique" du(des) problème(s)
=>
Démonstration et preuve (par un mathématicien?)
=>
Elaboration des algorithmes "prouvés" (par un informaticien?)

On peut voir ça comme ça effectivement, avec quand même la nuance importante que l'énoncé mathématique du problème ne sortira certainement pas en une seule étape de l'expression des besoins. Il y aura forcément de nombreux aller-retours (itérations comme on dit en Extreme Programming), ce qui fera que l'expression des besoins et l'énoncé mathématique du problème vont se contruire ensemble. Il y aura sans doute aussi besoin d'itérations à d'autres échelles.

[KiLVaiDeN]

Extreme Programming ! Noooooooon déjà qu'on est en open space, si en plus il faut qu'on se monte dessus pour programmer à deux sur une même machine, c'est foutu !

Pour Xave : je ne connais pas non plus les chiffres dont tu parles peux-tu éclairer celà, à moins que ton post était uniquement ironique ?

[xave]

Non, mon post était plutôt sarcastique.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

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.

Autant pour moi, c'est évidemment le contraire que je veux dire, (je ne parle pas exclusivement de l'utilisation de B), en résumé, c'est développez, soyez productifs et rapides, faites des applis maintenables et fiables mais faites le avec ce que vous avez sous la main, ne comptez sur aucun achat ni aucun investissement.

Quand aux résultats, je suis bien sûre que tout le monde a entendu parler des déboires d'Alstom ces dernières années.

Maintenant, je ne veux pas lancer une polémique sur une entreprise et son managment et je ne pense pas que c'était le but de ce post au départ, je vais donc m'en tenir là.

[DrTopos]

Autant pour moi, c'est évidemment le contraire que je veux dire, (je ne parle pas exclusivement de l'utilisation de B), en résumé, c'est développez, soyez productifs et rapides, faites des applis maintenables et fiables mais faites le avec ce que vous avez sous la main, ne comptez sur aucun achat ni aucun investissement.

Ce que tu dis là me semble refléter l'opinion de certains chefs de projet ou de certains patrons (pas spécifiquement chez Alstom d'ailleurs), et peut-être pas ton opinion personelle. Me trompe-je ?

Maintenant, je cite quand même la fin de la préface du B-Book:

Thanks to J.-R. Abrial, we now have an industrial method to build correct programs. We hope hat this book will convince the readers to save their money by using this method.

Pierre Chapront
Technical Director
GEC-Alsthom Transport

C'est moi qui ai souligné évidemment.

[xave]

Hum... non, non, c'est mon opinion, basée sur ma propre expérience chez Alstom (et ça remonte à avant que je sois chef de projet).

Jamais entendu parlé du B dans ma filiale...

[DrTopos]

Jamais entendu parlé du B dans ma filiale...

Tout cela est assez étonnant, puisque le B a été plus ou moins créé chez Alsthom (à l'époque où ça s'écrivait encore comme ça), et sponsorisé par Alsthom. Enfin, dans de si grosses boîtes il y a évidemment des cloisonnement étranges (il n'y en a pas que dans le secteur public !). Peut-être aussi que dans ta branche, de telle méthodes ne se justifient pas.