Discussion :

[kisitomomotene]

Une preuve est constructive quand elle satisfait des critères précis (et en général très mal connus, sauf des logiciens intuitionnistes). Mais tout ceci à une définition mathématique très précise, et le fait de détecter qu'une preuve est correcte et constructive est algorithmique en temps linéaire. L'extraction d'un algorithme d'une preuve constructive est une chose triviale ne posant aucun problème. De même, la transformation d'un algorithme en programme est un faux problème: un algorithme est un programme.

En conclusion, il est tout à fait certain que si on a une preuve mathématique correcte et constructive de l'existence d'une fonction, on peut en déduire mécaniquement un programme exempt de bug formel.

Un algorithme ou une demonstration constructive fait abstraction des environnements particuliers dans lequel un eventuel programme déduit devrait s'executer. Par exemple lorsque dans un programme vous ecrivez dans une variable, si l'environnement sous jacent n'est pas assez "robuste" et bien sécurisé, quelqu'un d'autre peut intentionnellement ou non modifier la valeur de cette variable, faussant ainsi le resultat votre programme, du point de vue de l'utilisateur c'est un BUG. Si vous êtes au courant de certainne insuffisance en terme de sécurité de la plateforme sous jacente dans laquelle s'éxecutera votre programme, vous allez ecrire votre programme en y ajoutant le code de sécurité. Un algorithme en général fait abstraction de ces conditions spécifiques qu'on peut rencontrer dans un environnement informatique donné.
L'algorithme "mathématique" est correct, lorsqu'on se limite à l'analyse. Au moment de la conception, et souvent même après le deployement du programme , on peut ajouter du code "système" à notre programme, pour résoudre les insuffisances, ou les particularités spécifiées ou non de l'environnement sous jacent.

En fait prouver qu'un programme s'execute sans BUG, implique la spécification précise de l'environnement sous jacent, ce qui n'est pas facile ( je dirais même impossible). Par exemple l'IDE Jbuilder 2005 ne s'execute pas bien avec certainne marque de carte graphique. Et c'était presque impossible pour les developpeurs de JBuilder de prévoir que certainne marque de carte graphique avaient "des ptits BUG" qui empêcheraient leur logiciel de fonctionner correctement, et leur permettant ainsi d'exclure ces cartes graphiques dans leur spécifications, ou bien de reécrire leur programme en tenant compte de cette situation.

[DrTopos]

Un algorithme ou une demonstration constructive fait abstraction des environnements particuliers dans lequel un eventuel programme déduit devrait s'executer. Par exemple lorsque dans un programme vous ecrivez dans une variable,

Comme je l'ai précisé, ce que j'ai dit sur les preuves et les programmes ne vaut que pour les programmes déterministes. Or l'affectation de variable est tout à fait non déterministe. Dans les programmes dont je parle il n'y a jamais d'affectation de variable, et donc le problème ne se pose pas.

Evidemment, je sais que pour quelqu'un qui est habitué à la programmation impérative, ne pas faire d'affectation de variable semble impossible. Simple question de culture de la programmation. Pour ma part j'ai écrit de nombreux programmes et même des gros programmes sans aucune affectation de variable, Evidemment, ce n'était ni en C ni en Java (mais éventuellement en Lisp, en Prolog en Caml ou en Anubis).

En fait le vrai problème vient du fait qu'il faut séparer les parties déterministes du programme des nécessaires parties non déterministes. Pour ce qui est du non déterminisme, il faut une modélisation du temps, et appliquer les méthodes de B ou des systèmes réactifs.

si l'environnement sous jacent n'est pas assez "robuste" et bien sécurisé, quelqu'un d'autre peut intentionnellement ou non modifier la valeur de cette variable, faussant ainsi le resultat votre programme, du point de vue de l'utilisateur c'est un BUG. Si vous êtes au courant de certainne insuffisance en terme de sécurité de la plateforme sous jacente dans laquelle s'éxecutera votre programme, vous allez ecrire votre programme en y ajoutant le code de sécurité. Un algorithme en général fait abstraction de ces conditions spécifiques qu'on peut rencontrer dans un environnement informatique donné.

Le système sous-jacent ne doit pas avoir d'insuffisance de sécurité. Si tu construits ta maison sur du sable, tu sais ce qui arrivera... Il faut maîtriser l'ensemble de la chaîne. Il ne faut pas écrire de programmes avec du code de sécurité pour pallier à des défaillances d'autres programmes. Il faut tout réécrire avec des méthodes sûres. C'est la seule voie raisonnable. Certains vont prétendre que c'est utopique, mais ce n'est pas du tout mon avis. Après tout il y a plein de gens qui se lancent dans l'écriture de systèmes d'exploitation 'from scratch'.

L'algorithme "mathématique" est correct, lorsqu'on se limite à l'analyse. Au moment de la conception, et souvent même après le deployement du programme , on peut ajouter du code "système" à notre programme, pour résoudre les insuffisances, ou les particularités spécifiées ou non de l'environnement sous jacent.

Meme remarque, il n'est pas question de mélanger du code prouvé avec du code de type Microsoft qui plante quand il en a envie (comme tu le reconnais toi même). Sinon, ça ne sert à rien de prouver. On ne peut pas faire ça à moitié. On le fait complètement ou pas du tout.

En fait prouver qu'un programme s'execute sans BUG, implique la spécification précise de l'environnement sous jacent, ce qui n'est pas facile ( je dirais même impossible). Par exemple l'IDE Jbuilder 2005 ne s'execute pas bien avec certainne marque de carte graphique. Et c'était presque impossible pour les developpeurs de JBuilder de prévoir que certainne marque de carte graphique avaient "des ptits BUG" qui empêcheraient leur logiciel de fonctionner correctement, et leur permettant ainsi d'exclure ces cartes graphiques dans leur spécifications, ou bien de reécrire leur programme en tenant compte de cette situation.

Parce que le constructeur de la carte ne respecte pas les spécifications. Si tu branches un truc qui marche sur un truc qui ne marche pas tu obtiens un truc qui ne marche pas. C'est évident.

Je n'ai jamais prétendu qu'on allait pouvoir appliquer les méthodes mathématiques avec les langages C, Java et similaires (C++, C#, etc...), ou encore en les mélangeant avec du code non prouvé, que ce soit du code système ou non. Il est bien clair que les méthodes mathématiques ne peuvent être appliquées que si on maitrise la chaîne logicielle de bout en bout, et si on peut faire confiance au hardware.

Pour le hardware, en général ça va (à part sans doute quelques cartes pour lesquelles les ingénieurs étaient trop pressés pour faire les choses proprement). Encore qu'il reste beaucoup d'efforts à faire dans les spécifications du hardware. Autant dire que le 'plug-and-play' me fait doucement sourire. Par contre, en matière de programmation, j'ai bien précisé que ce n'est pas avec les langaages habituels qu'on risque d'y arriver.

[kisitomomotene]

Comme je l'ai précisé, ce que j'ai dit sur les preuves et les programmes ne vaut que pour les programmes déterministes. Or l'affectation de variable est tout à fait non déterministe. Dans les programmes dont je parle il n'y a jamais d'affectation de variable, et donc le problème ne se pose pas.

Evidemment, je sais que pour quelqu'un qui est habitué à la programmation impérative, ne pas faire d'affectation de variable semble impossible. Simple question de culture de la programmation. Pour ma part j'ai écrit de nombreux programmes et même des gros programmes sans aucune affectation de variable, Evidemment, ce n'était ni en C ni en Java (mais éventuellement en Lisp, en Prolog en Caml ou en Anubis).

êtes vous sûr que lors de la translation de ces programmes en assembleur ou en langage machine on n'aura pas des affectations? Tous les langages sont des abstractions de l'assembleur ou du langage machine. Pour être sûr qu'on n'effectue pas d'affections, il faudrait demontrer que l'équivalent en assembleur ou en langage machine des instructions qu'on a utilisée en Lisp ou Prolog ne comporte pas d'affectation.

En fait le vrai problème vient du fait qu'il faut séparer les parties déterministes du programme des nécessaires parties non déterministes. Pour ce qui est du non déterminisme, il faut une modélisation du temps, et appliquer les méthodes de B ou des systèmes réactifs.

Je ne crois pas qu'un problème posé peut avoir une solution déterministe globale, il y aura toujours des variantes non déterministe . Je prend un exemple:

Si vous voulez ecrire un programme pour calculer l'intégral d'une fonction numérique quelconque continue dans R.
En prouvant l'existence de cette intégral peut être par la construction des trapèze, on pourra déduire un algorithme "mathématique". Par la suite on peut avoir un programmme informatique P1 qui est une déduction trivial de l'algorithme "mathématique".

Ce programme P1 peut bien marcher dans en environnement donné.
Dans un autre environnement peut être pour des besoins de performance, on peut décider d'installer ce programme sur un serveur puissant, et les autres postes de travaill ( de faible puissance) utiliseront le programme à distance. Donc il faut ajouter à P1 du code pour la distribution, et du code pour le rendre "Thread-safe". On obtient un autre programme P2.

Pour le même problème, on a un seul algorithme "mathématique", mais on a deux programme informatiques P1 et P2. P1 peut être déterministe dans un environnement bien défini. Mais P2 par sa nature est indéterministe ( car il est distribué).

Comme il y a tjrs des variantes "indéterministes" dans un problème "réel", et ces variantes "indéterministe" n'ont pas tous des modèles mathématiques (j'aimerais que quelqu'un me donne un modèle mathématique d'un environnement informatique distribué) on ne peut pas pour l'instant faire de l'informatique comme si on faisait des mathématiques.

[DrTopos]

êtes vous sûr que lors de la translation de ces programmes en assembleur ou en langage machine on n'aura pas des affectations?

Bien sûr que la traduction en assembleur introduit des affectations. A la limite, il n'y a même plus que cela. On simule le calcul déterministe avec un automate à pile. C'est normal. Ce genre de traduction ne peut pas introduire de faute si elle est bien faite. On peut facilement faire la preuve que cette traduction est correcte.

D'ailleurs, j'ai sous la main un exemple d'une telle preuve. Il s'agit d'un problème d'examen que j'ai posé en maîtrise de maths (option informatique théorique) à l'époque où j'enseignais à Nantes. Je te convie à faire ce problème, que tu peux trouver ici. On y traduit un langage complètement déterministe en instructions de manipulations de registre et pile, et on prouve que tout est correct.

Tous les langages sont des abstractions de l'assembleur ou du langage machine.

Tous non. C'est un point de vue beaucoup trop réducteur. En tout cas, je ne vois pas du tout les choses comme ça. Quand j'ai conçu Anubis, je n'ai pas du tout pensé aux machines ou à l'assembleur. Je n'ai pensé qu'aux catégories bicartésiennes fermées. Autrement-dit je suis allé progressivement du haut niveau (le langage) vers le bas niveau (la machine virtuelle), alors que ton affirmation laisse entendre que pour faire un langage il faudrait partir obligatoirement du bas niveau pour abstraire vers le haut niveau.

Il est vrai que c'est ce qui c'est passé pour le C, qui est manifestement une abstraction de la machine. Par contre, Lisp, Prolog, Caml ou Anubis, n'ont pas du tout été conçus de cette façon, mais à partir d'une théorie: le lambda-calcul pour Lisp, la logique du premier ordre pour Prolog, la théorie des types pour Caml et la théorie des catégories pour Anubis.

Par ailleurs, ce que tu dis à la suite de ton exemple d'intégrale est juste un problème de réalisation. Il est bien clair que si on a un algorithme prouvé, il faut aussi le réaliser proprement. C'est un peu le même problème que celui de la traduction en assembleur, et il peut se traiter aussi facilement et une fois pour toutes. Il faut qu'on soit sûr du matériel et de la façon dont les algorithmes sont implémentés (que ce soit partagé ou non). C'est un problème indépendant de celui de prouver les programmes. Prouver que le support de calcul (machine ou réseau de machines) calcule correctement relève d'une preuve indépendante de la preuve du programme lui-même, et qui doit être faite préalablement et une fois pour toutes. Ceci dit, autant je sais prouver qu'un compilateur est correct, autant je ne me suis pas essayé sur les réseaux. Il est vrai qu'il y a encore beaucoup de travail à faire de ce coté. Mais à mon avis ça relève simplement de la logique de Hoare (précondition-postcondition), qui est la façon normale de faire des preuves d'automates, qu'ils soient distribués ou non.

Il est bien certain qu'une preuve mathématique ne donne des certtitudes qu'à propos des mathématiques. Il y a toujours un moment où il faut modéliser la réalité physique. Et là évidemment, on ne peut pas avoir de certitude absolue. Je suis bien d'accord. Mais encore une fois c'est une autre question. Ce fait ne dispense pas d'essayer de rendre plus sûre toute la partie du développement qui relève des mathématiques. Pour prendre une comparaison, ce n'est pas parce que le lancement d'un satellite présente des aléas, qu'on ne doit pas faire le maximum pour prouver que la partie formelle du travail est correcte.

[kisitomomotene]

Pour prendre une comparaison, ce n'est pas parce que le lancement d'un satellite présente des aléas, qu'on ne doit pas faire le maximum pour prouver que la partie formelle du travail est correcte.

Ok je suis parfaitement d'accord avec vous. On devrait tjrs prouver que la partie formelle d'un programme est juste. Et ça beaucoup de programmeur ne le font pas, peut être parceque les langages les plus utilisés actuellement ne permettent de le faire à l'intérieur même du programme.

En fait existe t'il un langage qui puisse permettre justement de prouver qu'un programme est formellement juste. C'est à dire si vous commettez une erreur "logique", il vous le signale au moment de la compilation., un peu comme un prof détecte une erreur de raisonnement dans une démonstration de son élève ?