Discussion :

[DrTopos]

Bonjour à tous.

InOCamlWeTrust --> Merci pour les informations à propos d'Airbus. C'est tout à fait intéressant.

Par contre, j'ai une petite remarque à faire sur ton discours. Il faudrait savoir ce que signifie ``prouver un compilateur''. Je sais ce que veut dire ``prouver un énoncé'', mais ``prouver un compilateur'' n'est pas tout à fait clair. Cela veut certainement dire prouver un certain énoncé en rapport avec le compilateur, mais lequel ?

Par ailleurs, en ce qui concerne le fait de se prouver soi-même, le second théorème d'incomplétude de Gödel dit qu'un système qui prouve sa propre consistance ne peut être qu'inconsistant. Evidemment, prouver un compilateur n'est peut-être pas la même chose que prouver une consistance logique. Mais quand même, il me semble que prouver Coq en Coq ne prouve rien, où alors, il y a un élément externe participant à cette preuve.

Par ailleurs, le fait qu'un problème soit NP complet n'empêche nullement de le résoudre, même en supposant P != NP, pourvu que les données ne soient pas trop volumineuses et qu'on dispose d'assez de temps. C'est certainement ce qu'il se passe en patique avec LUSTRE. Il serait intéressant d'obtenir des détails (puisque tu sembles avoir tes entrées chez Airbus) sur les temps mis par les compilateurs LUSTRE pour optimiser les automates d'une taille donnée.

[DrTopos]

Cependant, force est de constater que dans une équipe de développement [...], il serait vain d'essayer d'obtenir des gens qu'ils fassent des démonstrations mathématiques de la sûreté de leurs réalisations.
Si l'on est particulièrement maladroit dans la formulation de ses demandes de preuves dans son équipe de développement, on peut même provoquer un rejet total des preuves de toutes natures qu'elles soient.

Eviter dans la programmation courante les mathématiques autant que possible, à cause de leur côté repoussoir, dissuasif.

Ah que tout cela est attristant ! Non pas tellement pour les informaticiens, mais pour les profs de maths, qui n'atteigent donc pas leur but, qui devrait être de communiquer le plaisir de faire des maths.

Il est navrant d'apprendre que les mathématiques sont un repoussoir dans les équipes de développeurs. Moi qui ait fait plus de 20 ans d'informatique, et encore plus de maths, et sans vouloir défendre une quelconque chapelle, je n'ai jamais trouvé les mathématiques repoussantes, mais il m'est arrivé de trouver certains concepts informatiques, inutilement compliqués, bourrés de choses faisant double emploi, et exempts de toute justification théorique, parfois très repoussants, pour ne pas dire qu'ils me rendent carrément malade. Après toutes ces expériences, je trouve que les maths sont, dans les principes, plus simples que l'informatique. Il y a donc certainement ici des idées reçues à propos des maths extrèmement néfastes pour le progrès des techniques.

[InOCamlWeTrust]

Prouver un compilateur revient à démontrer sa correction, c'est-à-dire que le programme produit est sémantiquement équivalent au programme fourni en entrée.

Pour ce qui est de la logique, Gödel et compagnie, je ne peux rien en dire car je ne suis pas assez calé sur le sujet, même si la question m'intéresse : le mieux serait de demander aux concepteurs de Coq eux-mêmes comment ils ont fait. Lorsque je disais que l'on écrivait Coq, le compilait, puis prouvait ses sources grâce à lui-même, c'est une hypothèse de démarche que je fais-là (je ne vois pas, grosso-modo, comment on pourrait faire autrement), mais très certainement, la réalité ne doit pas être bien différente.

Une fonctionnalité très intéressante de Coq : extraction automatique de programmes OCaml, Haskell ou Scheme à partir de leur preuve !

http://coq.inria.fr/V8.1/refman/index.html

La racine du document est ici :

http://coq.inria.fr/V8.1/refman/index.html

et le site là :

http://coq.inria.fr/coq-fra.html

Concernant les optimisations des automates en Lustre, je n'en sais rien car j'en suis resté à un niveau plus ou moins utilisateur de ce langage (Esterel m'intérsse finalement plus, car Lustre est trop orienté langage pour automaticiens) : très certainement, l'optimisation doit être assez agressive car le langage s'y prête très bien.

A l'origine, Lustre était destiné à implanter des circuits dans des FPGA, mais aujourd'hui, c'est devenu un langage de programmation à part entière : la raison est, selon moi, qu'il n'y a aucune perte de performances entre l'implantation matérielle de ces circuits sur FPGA (les FPGA les plus performants actuellement doivent monter à 100-200 MHz) et leur émulation par programmes sur de vrais processeurs (et par la même occasion, pouvoir implanter plusieurs circuits différents en parallèle sur le même processeur) ; cependant, là encore, il serait intéressant de demander aux gens de chez Airbus ou Schneider Electric, car ce sont ces derniers à l'orgine du projet.

[grunt2000]

@DrTopos: c'est vrai que j'y vais fort sur les mathématiques.

Ce que veux mettre en avant, c'est qu'il est par nature délicat d'obtenir des équipes de développement qu'elles mettent en place des préconditions, assertions et post-conditions simples, claires, et en rapport avec thème du problème abordé.

Le faire selon une démarche informaticienne (état initial et final, action, conditions) me semble possible.
Mais le faire selon une démarche mathématicienne (preuves, variants & invariants, avec démonstrations de logique formelle) ne peut pas être à la portée de qui n'a jamais vécu avec le concept d'une assertion auparavant.

Par là, je suis méfiant.
Une équipe de développeurs comprend parfois des membres qui ont été initiés à quelques principes de sûreté de fonctionnement. Mais ce n'est pas si fréquent. Et alors, le travail à mener est de longue haleine. Il s'agit de ne pas présenter trop tôt des principes qui apparaitraient hors de portée aux interessés sous peine de les faire fuir.

Personnellement, je n'accepte pour "preuve" dans un programme qu'une expression telle que pour une fonction répondant à un besoin exprimable pour un utilisateur non informaticien (c'est essentiel), la démonstration mathématique prétendue probante mentionne:
- l'état initial et final
- la nature de l'action vérifiée
- les conditions servant à la vérification

dans un vocabulaire intelligible au dit utilisateur, et d'une manière qu'il peut la comprendre.
Faute de quoi, il me semble que ce que je lirais ce sera du bruit.


L'établissement d'une preuve ne doit pas engendrer une perte de clarté.
Et l'emploi d'expressions mathématiques au sein d'un code source tend à me gêner pour cette raison.

[gorgonite]

tiens, ça révolutionne ce que je connaissais de la logique... n'est-il pas impossible de prouver une théorie grâce à cette même théorie ?

c'est de cela dont je voulais parler

Par ailleurs, en ce qui concerne le fait de se prouver soi-même, le second théorème d'incomplétude de Gödel dit qu'un système qui prouve sa propre consistance ne peut être qu'inconsistant.

------------------------------------

Je ne vois pas vraiment ce à quoi tu fais référence, peut-être à autre chose... Il y a plusieurs types d'algorithmes : à priorité variable ou constante. Dans les deux cas, on sait trouver des algorithmes assez simples optimaux. Dans certains cas même, on sait établir des conditions nécessaires et suffisantes d'ordonnançabilité des processus.

je fais référence à la recherche de l'ordonnancement optimal des instructions assembleurs générées par un compilateur (qui est plus dans mon domaine de compétences). A ma connaissance, il existe une heuristique qui amène à l'optimal + 1, mais la recherche de l'optimal est toujours NP-Complet

quand est-ce que l'on enseignera des choses utiles et non des conneries d'informaticiens théoriques ?

modères tes propos... je te rappelles que je fais de l'info théorique, et tes futurs collègues aussi

Ben... t'as pas de bol ! Esterel est un langage ou l'on manipule des évènements pouvant arriver à n'importe quel moment (comme les signaux en C, qui sont asynchrones) : le langage en lui-même ne possède pas de notion d'horloge, dont chaque top détermine une "action" particulière à traiter. Ce n'est pas le cas en Lustre, langage qui est régi par la notion d'horloge : horloge courante, sous-échantillonnage et sur-échantillonnage sur des horloges différentes.

je connais esterel, et maintenant que j'ai relu mon cours de concurrence, j'ai le modèle logique sous-jacent...
par ailleurs, ce n'est pas parce qu'un langage a un coeur synchrone qu'on ne peut faire des traitements "quasi-asynchrones" dessus... qui te dit que cela ne réagit pas au toc suivant la réception du signal

Ils sont pas un peu bizarres tes profs ?

étant donné que Esterel nous a été présenté par Gerard Berry, je pense que l'on a eu une bonne description de ce que c'était...

pour infos, mes profs de systèmes synchrones étaient Marc Pouzet et Jean Vuillemin... qui sont loin d'être bizarres
http://mpri.master.univ-paris7.fr/C-2-23-1.html

[Caine]

Bonjour à tous,

Je tiens à réagir à l'opinion quelque peu négative exprimer contre les développeurs...

Je me considère comme un oldies (à 35 ans) car ma formation dans le métier incluée des notions visiblement de moins en moins enseigner. Justemment comme les mathématiques adaptées à l'info, la preuve de programme en étant un module, avec la théorie des graphes.

Toute une génération d'ingénieur est sortie avec les même connaissances que moi. Mais dès ma première expérience, alors que j'appliquais les fondements appris à la fac, on m'a clairement intimer de laisser tomber "ses conneries inutiles";il fallait du time-to-market!

Pas le temps pour des algorithmes, de la preuve de programme, de l'abstraction de données.

Il y a bien sûr trop de développeurs qui ont trouvé ses matières inutiles, mais heureusement il y a aussi leur contraire.

Hélas, après des années d'expérience où ils obéissent à la loi du time_to_market, il ne leurs reste plus grand chose de ses fameux fondamentaux.

Notez bien que je ne me sens pas vexé par vos propos. Il me semblait juste important de rajouter un peu d'eau dans le vin

[HS] Dr Topos, je vous demande la permission d'ajouter ceci à ma signature:
"Un langage puissant, une syntaxe concise et claire; allier la portabilité de Java, la souplesse du C et la rigueur de l'ADA.
Lien vers le site du langage Anubis"

[DrTopos]

Bonjour à tous.

Je tiens à réagir à l'opinion quelque peu négative exprimer contre les développeurs...

En ce qui me concerne, je n'ai compris les propos de grunt2000 que comme citant un exemple. Il est bien clair qu'il doit y avoir des exceptions. Toutefois, j'ai peur qu'elles ne soient pas légion.

Toute une génération d'ingénieur est sortie avec les même connaissances que moi. Mais dès ma première expérience, alors que j'appliquais les fondements appris à la fac, on m'a clairement intimer de laisser tomber "ses conneries inutiles";il fallait du time-to-market!

Je sais, par quelques amis qui ont vécu cela dans des entreprises de developpement de soft, qu'il est souvent très difficile de discuter avec le chef, qui bien souvent croit tout savoir mieux que tout le monde, sous pretexte qu'il a un diplôme de telle ou telle école. Par conséquent, les gens qui ont éventuellement de la rigueur scientifique sont bridés par ceux qui ont le pouvoir (et qui en général sont plutôt à orientation management que scientifique), et qu'on pousse de plus en plus, semble-t-il, dans des stratégies à court terme. J'espère qu'il y aura un jour un retour de balancier.

Il y a bien sûr trop de développeurs qui ont trouvé ses matières inutiles, mais heureusement il y a aussi leur contraire.

On est bien d'accord.

Notez bien que je ne me sens pas vexé par vos propos. Il me semblait juste important de rajouter un peu d'eau dans le vin

Loin de moi l'idée d'avoir voulu vexer qui que ce soit. Je n'exprimais que ce qui me semble être une tendance générale.

[HS] Dr Topos, je vous demande la permission d'ajouter ceci à ma signature:
"Un langage puissant, une syntaxe concise et claire; allier la portabilité de Java, la souplesse du C et la rigueur de l'ADA.
Lien vers le site du langage Anubis"

Mais bien sûr. Je ne pense pas d'ailleurs qu'il ait besoin d'une autorisation pour cela. Chacun peut donner son avis sur Anubis, qu'il soit positif ou négatif, sans me consulter. N'en fait-on pas autant à propos des autres logiciels ?

Cordialement.

[Caine]

DR Topos => Je ne voulais pas dire que les propos étaient vexant, juste m'assurer que ma réaction ne soit pas comprise comme telle.

Je trouve normal de demander votre autorisation, par politesse et respect. Après tout avant de donner une avis sur un langage je pense qu'il faut l'avoir quelque peu manié.

Or, vous auriez de part votre position particulière de créateur du langage, pu estimer que ma comparaison dans la signature était erronée.

J'espère qu'il y aura toujours plus de gens pour essayer le langage.

Désolé pour cette digression dans le fil de la discussion.

[grunt2000]

Less projets du monde libre, que l'on trouve chez sourceforge ou apache, sont intéressants à examiner dès lors qu'ils ont passés une version 1.0.0 en release, et qu'ils jouissent d'une diffusion/popularité suffisante.

Je serais bien en peine de faire des statistiques sur l'ensemble de ces projets. Mais il me semble en avoir vu peu qui emploient des techniques de programmation garantissant la sûreté de fonctionnement.
Et cela est révélateur, tout comme l'est la remarque de Caine qui dit "Toute une génération d'ingénieurs est sortie avec les même connaissances que moi". Car le problème est la proportion conséquente de développeurs non formés (aux techniques de sûreté de fonctionnement).
La population informaticienne est loin, très loin, d'appartenir en majorité à la branche des ingénieurs. J'ajoute qu'en faire partie ne garantit en rien que l'on sera convaincu d'utiliser ces techniques.

Le problème est ce que l'on oppose à cette situation.
Car il me semble aujourd'hui que tout est noir ou blanc.

Noir: s'il n'existe aucune preuve dans un traitement ; on n'en doutera pas.

Blanc: s'il faut que les preuves soient si formelles, si strictes, que le prix de leur qualité est l'acquistion de logiciels et de collaborateurs triés sur le volet, assortis d'une formation avancée.

Permettez-moi de militer pour le gris.
Des solutions intermédiaires doivent être promues. Des techniques de sûreté de fonctionnement moins abouties, mais peut-être plus claires, plus accessibles, qui auraient naturellement un côté "probant" plus faible que celles basées sur les mathématiques et les démonstations de logique formelle.
Mais qui auraient pour atout d'être plus populaires, d'apparaître plus fréquemment. C'est qu'il faut trouver un moyen de propager des pratiques vertueuses qui aujourd'hui - sauf dans des industries "extrêmes" - semblent concerner trop peu les réalisateurs.

[PINGOUIN_GEANT]

Je n'ai pas tout lu, mais je peux dire ce que l'on fait chez Airbus.

Concernant les programmes, ils sont entièrement écrits en Lustre, langage trivial à prouver, dont le compilateur lui-même a été prouvé, car écrit en Objective Caml, le compilateur Objective Caml étant lui-même prouvé... et écrit en Objective Caml. Le programme de preuve, Coq je pense, s'est prouvé lui-même, et comme il a aussi été écrit en Objective Caml, la boucle est bouclée !

Les seules parties écrites en C dans le code embarqué concernent les entrées-sorties, que l'on ne peut pas faire en Lustre.

Je suis un peu étonné que le produit SCADE est basé sur OCaml. Je n'ai pas trouvé de trace de Ocaml sur le site d'Esterel (ne pas confondre avec le langage Esterel), donc je suppose que c'est faux.

EN suivant le lien, vous verrez des informations intéressantes sur le générateur de code certifié DO178-B (process à respecter pour concevoir les systèmes embarqués de l'avion), notamment que l'allocation dynamique est interdite.

[Montaigne]

Concernant les programmes, ils sont entièrement écrits en Lustre, langage trivial à prouver, dont le compilateur lui-même a été prouvé, car écrit en Objective Caml, le compilateur Objective Caml étant lui-même prouvé... et écrit en Objective Caml. Le programme de preuve, Coq je pense, s'est prouvé lui-même, et comme il a aussi été écrit en Objective Caml, la boucle est bouclée !

Coq ne s'est pas prouvé lui même : ils ont sacrifié un thésard pour le faire. Il n'a pas tout fait d'ailleurs...

[gorgonite]

Coq ne s'est pas prouvé lui même : ils ont sacrifié un thésard pour le faire. Il n'a pas tout fait d'ailleurs...

et il l'a fait avec Coq ?

si oui, le pauvre... il a du en baver, parce que la logique intuitionniste, cela rallonge les démos

[DrTopos]

et il l'a fait avec Coq ?

si oui, le pauvre... il a du en baver, parce que la logique intuitionniste, cela rallonge les démos

Ce n'est pas la logique intuitionniste qui rallonge les démonstrations, car les moyens de preuve de la logique intuitionniste font tous partie aussi de la logique classique et à vrai dire la différence est minime, car elle se limite aux conséquences de l'axiome du choix (à condition de pouvoir démontrer le théorème de Diaconescu dans le système considéré).

Ce qui rallonge les démonstrations dans le cas de Coq, est à mon avis le fait que le principe d'indiscernabilité des preuves n'étant pas appliqué partout en Coq (contrairement à ce qu'il se passe en mathématiques usuelles), un même énoncé peut avoir plusieurs preuves distinctes. Dès lors, pour prouver un énoncé, il ne suffit plus de s'assurer qu'une preuve existe (et de laisser le système se débrouiller pour boucher les trous dans les preuves), il faut trop souvent sans doute en exhiber une explicitement. Par ailleurs, la syntaxe même de Coq, qui est un tant soit peu exotique par rapport à celle des maths usuelles, doit aussi y être pour quelque chose. Et puis, il y a un autre facteur qui joue sans aucun doute un rôle important, qui est le fait que pour prouver un compilateur ou plus généralement un programme, le plus dur n'est pas de prouver, mais de formaliser l'énoncé à prouver.

Ceux qui veulent en savoir plus sur l'indiscernabilité des preuves pourront lire mon exposé fait récemment à Marseille-Luminy qui est consacré à ce sujet.

[gorgonite]

Ce n'est pas la logique intuitionniste qui rallonge les démonstrations, car les moyens de preuve de la logique intuitionniste font tous partie aussi de la logique classique et à vrai dire la différence est minime

sans le tiers exclu, il n'est pas trivial de prouver que racine de 2 n'est pas rationnel... (exemple classique )

j'ai appris cette année que la logique intuitionniste impliquait un "constructivisme" et que donc si l'on voulait montrer l'existence de quelque chose, on était en gros obligé de donner un algo pour le construire... (enfin, je ne suis pas bon sur les logiques IL ou LL )

[DrTopos]

Bonjour à tous.

Je signale à tous ceux que la possibilité de preuver des énoncés dans un langage de programmation intéresse, qu'un fil consacré à cette question est ouvert dans le forum ``Langage fonctionnels''. Ce fil est sous forme de quizz, et vous êtes tous cordialement invités à participer.

[pikatchou06]

Je voulait clarifier ce qui est fait actuellement chez Estérel:

1) Le compilateur Scade 5.1, écrit en C, est un compilo Scade -> C
Ce compilateur est qualifié, il est écrit en respectant la norme DO-178B.

2) Le compilateur Scade 6.0, écrit en OCaml, est un compilo Scade -> C
Il n'existe pas encore de version "Qualifiée" de ce compilateur (Qualifiée au sens de respectant la DO-178b), mais sa sortie est prévue.

3) Airbus n'utilise que la version 5.1 pour le moment. Donc pas de OCaml chez airbus.

Enfin, concernant les preuves de programmes, cette pratique n'a aucune valeur pour la DO actuelle. C'est à dire que un programme avec une preuve de correction est considéré de la même mannière qu'un programme sans, ce qui permet sa "certification" c'est le process qui a été employé pour l'écrire et le valider.
Des évolutions sont attendue de ce côté dans la DO version C, qui devrait sortir un de ces 4 matins.