Discussion :

[alex_pi]

Une question au créateur d'Anubis2 :

Sachant qu'un solveur de Sudoku s'écrit en une vingtaine de lignes en OCaml, et en un peu plus de 5000 lignes (en comptant néamoins les commentaires) en Coq, le tout accompagné d'une notice de 13 pages en PDF, où se situera l'équivalent en Anubis2 et quelles seront les assurances données ? Juste que ça termine, ou bien que ça retourne toujours la bonne solution si elle existe ?

Merci

[DrTopos]

Une question au créateur d'Anubis2 :

Sachant qu'un solveur de Sudoku s'écrit en une vingtaine de lignes en OCaml, et en un peu plus de 5000 lignes (en comptant néamoins les commentaires) en Coq, le tout accompagné d'une notice de 13 pages en PDF, où se situera l'équivalent en Anubis2 et quelles seront les assurances données ? Juste que ça termine, ou bien que ça retourne toujours la bonne solution si elle existe ?

Merci

C'est sans doute dû au problème posé (Sudoku) plus qu'à la structure de COQ. Par ailleurs, je ne sais pas ce que cette preuve prouve précisément. Sans doute pas seulement la terminaison.

Bien entendu, écrire un algorithme est une chose, prouver qu'il a telle ou telle propriété en est une autre, et il n'y a aucune correlation a priori entre les tailles des deux textes. Un exemple très simple est le problème de Syracuse: On a la fonction f suivante, définie sur les entiers et à valeurs dans les entiers

Code :

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

1
2
3
4
f(1) = 1
f(n) = f(n/2) si n est pair
f(n) = f(3n+1) sinon

Ces trois lignes forment un programe de calcul très simple. La question est qu'il n'y a aucune garantie qu'il termine. Prouver qu'il termine (ça sera forcément sur la valeur 1 d'ailleurs tel qu'il est écrit ici) est encore une conjecture aujourd'hui. Si un jour on en trouve une preuve, il est probable qu'elle sera monstrueuse.

Le programme ci-dessus peut être écrit en Caml et en Anubis 1, mais pas en Anubis 2, tant qu'on ne saura pas démontrer que ça termine. En effet, le compilateur Anubis 2 oblige le programmeur à passer sous les fourches caudines des schémas de récursion. C'est l'un des éléments qui assurent que tous les programmes Anubis 2 purs terminent. je ne parle bien sûr que des programmes purs (aucune manipulation d'objet concrêt).

Je pourrais d'ailleurs prendre un autre exemple pour montrer la différence de philosophie. Imaginons qu'on veuille écrire un programme pour réduire les termes du lambda-calcul typé. C'est très simple d'itérer la beta-réduction, et on peut faire un programme Caml très court faisant cela. Par contre, un programme en Anubis 2 pur faisant la même chose contient nécessairement une preuve du théorème de Tait. Il est donc certainement beaucoup plus long, et évidemment très loin d'être trivial. Je suppose qu'il en serait de même en COQ.

Pour ce qui est du Sudoku, tout dépend de ce qui est prouvé. S'il s'agit à la fois de la terminaison, de l'unicité ou du caractère optimal de la solution, que sais-je encore, ça peut être long effectivement. Pour ce qui est des assurance données et de la taile de la preuve, cela devrait être comparable à ce qu'on fait en COQ. C'est plus la nature du problème qui compte que le langage.

Ce qui est surtout important dans l'industrie est le fait que le programme fasse ce qu'on veut qu'il fasse. Le meilleur moyen de s'en assurer reste quand même de se donner des moyens formels de preuve. C'est ce qui a été fait pour le logiciel de la ligne 14 du métro, fait en système B. Le source est certainement plus long que ce qu'il aurait été sans les preuves, mais on a sans doute jugé que l'investissement était rentable. On n'a jamais constaté de bug sur ce programme. On a donc évité les frais de mise au point, les ennuis et le stress. De toute façon la sécurité a un prix, et plus ça va plus on exige de sécurité, et plus on est prêt à payer pour cela. Je pense donc que l'avenir est aux langages à preuves, même si cela doit changer la façon de tavailler des développeurs.

Pour en revenir quand même à Anubis 2, je fait tout pour qu'il soit très proche des maths usuelles. C'est bien sûr un des aspects importants sur lequels je mise.

[alex_pi]

C'est sans doute dû au problème posé (Sudoku) plus qu'à la structure de COQ. Par ailleurs, je ne sais pas ce que cette preuve prouve précisément. Sans doute pas seulement la terminaison.

Non, probablement pas ! Je pense que ça prouve que s'il existe une solution, il la trouve, que s'il en existe plusieurs, il les trouve toutes, etc. (en plus de la terminaison, qui est une nécessité en Coq)

Bien entendu, écrire un algorithme est une chose, prouver qu'il a telle ou telle propriété en est une autre, et il n'y a aucune correlation a priori entre les tailles des deux textes.

L'indécidabilité nous enquiquinera toujours...

Ce qui est surtout important dans l'industrie est le fait que le programme fasse ce qu'on veut qu'il fasse. Le meilleur moyen de s'en assurer reste quand même de se donner des moyens formels de preuve.

Je vous ai envoyé mon cursus actuel par MP, vous vous doutez bien que je ne vais pas faire une opposition frontale ! Mais je ne suis néamoins pas entièrement d'accord. Il y a des domaines où l'ont veut avoir des assurances que ça se passe bien. Quand on conduit un Métro, on fait appelle au système B et à ses boites, quand on pilote un A380, on fait vérifier son code par Astrée, et je suis bien content qu'un compilateur C certifié soit en bonne voie. En revanche, je pense que le cas du sudoku est parlant. Quand on voit que l'on multiplie le nombre de ligne par plus de 100, et que la seconde version nécessite probablement un niveau bac+4 pour être comprise, et bac+5 pour être écrite, on se dit que non, ce n'est pas "l'Avenir", avec un grand 'A'. On n'est pas pret de prouver que le noyau de mon OS ou même mon client mail font exactement ce que l'ont veut, et tant pis (et d'ailleurs, heureusement qu'on ne prouve pas qu'ils terminent, ça m'ennuierai :-))


Et c'est la raison de ma question sur Anubis2. Si c'est un système de preuve complet, en quoi sera-t-il plus utilisable par un humain normal que Coq (qui est, admettons le, plutot ardu à appréhender), ou qu'apportera-t-il par rapport à ce qui existe déjà. Si ce n'est pas le cas, qu'aportera-t-il de plus qu'un typage statique fort "à la ML", et surtout, à quel prix ? Pour écrire un solveur de sudoku dont on prouvera simplement qu'il termine, sans forcément prouver quoi que ce soit sur la solution, à combien entre 20 et 5000 lignes de code évaluez vous la chose ? Bref, peut-on en savoir un peu plus que "il s'appuie sur les mathématiques" ce qui veut tout dire et rien à la fois ?

[DrTopos]

Il est tard et je ne pourrai pas répondre sans doute avant mercredi (j'enseigne les lundis et mardi). En attendant, je te recommande ce document qui est assez instructif:

http://www.univ-valenciennes.fr/ROI/...rian-Petit.pdf

[InOCamlWeTrust]

quand on pilote un A380, on fait vérifier son code par Astrée

Très certainement Astrée a du jouer un rôle important pour l'A380, mais leur techniques de génération de code et de programmes sont beaucoup plus poussées que ce que l'on pourrait croire. Entre autres, l'utilisation de Lustre facilite grandement la tâche. On n'écrit quasiment pas de code C embarqué chez Airbus : les seules parties écrites en dûr, en C, sont celles concernant les entrées-sorties, que l'on ne peut faire en Lustre. Tout le reste, c'est du Lustre.

Ca c'est ce qui concerne l'avionique... bien-sûr, le serveur de films embarqué n'est pas fait comme ceci... si il tombe en panne, c'est pas trop grave... tout au plus on s'ennuira un peu pendant le voyage !

[alex_pi]

On n'écrit quasiment pas de code C embarqué chez Airbus : les seules parties écrites en dûr, en C, sont celles concernant les entrées-sorties, que l'on ne peut faire en Lustre. Tout le reste, c'est du Lustre.

Je ne sais pas, mais au final, il y avait quand même plus de 500 000 lignes de code C à vérifier ! C'est un peu long à la main :-) Après, ce code C est peut-être une compilation de Lustre, je n'en sais rien.

[SpiceGuid]

Je suis tout comme toi dans le questionnement, tout comme toi je me hasarde à faire des suppositions, ici j'en fais deux:

• Si un jour je peux lire une source COQ ce sera grâce à DrTopos qui m'a considérablement déblayé le terrain, COQ pourrait me paraître beaucoup plus accessible qu'il me paraîssait il y a peu. En tout cas je n'ai pas connaissance d'un tutoriel sur le sujet qui soit plus accessible que le quizz de DrTopos.
• Je ne crois pas que la longueur de la preuve soit un critère, et ce quelle que soit la façon dont on la mesure.

Par contre je m'intéresse à la qualité de la preuve:

• Est-elle facultative ou obligatoire ? Intuitivement je dirais facultative parce que le type de (x:One) |-f-> f x est One -> $T et celà me paraît un type valide. Si j'ai raison celà répondrait un peu à ta question: contrairement à COQ et Epigram le langage des termes serait Turing-complet. Dans tous les cas le langage des énoncés n'est pas Turing-complet. COQ et Epigram t'obligent à travailler avec le langage des énoncés. Avec Anubis 2 tu écrirais des termes que tu pourrais ensuite décorer avec des énoncés.
• Est-elle incrémentale ? Par exemple je viens de programmer un AVL. Si la preuve est facultative je peux ne rien prouver du tout. Puis dans un élan salvateur je peux vouloir prouver que je construis et maintiens bien un ABR, juste en ajoutant des énoncés, sans toucher à l'implémentation. Enfin je serais bête de pas prouver que mon ABR est équilibré, toujours en ajoutant des énoncés, sans toucher à l'implémentation. Tu ne peux pas le faire en COQ ou Epigram parce que tu ne peux pas créer une expression sans écrire exhaustivement son énoncé.

Par rapport à ML/Haskell, Anubis 2 ajoute une nouvelle couche de typage (facultatif). COQ ou Epigram jettent tout le système auquel tu es habitué, tu ne peux plus écrire let rec f () = f ();; car c'est tout simplement mal typé.

Honnêtement, je ne connais pas actuellement d'autre proposition capable d'augmenter le typage à la ML comme je crois qu'Anubis 2 pourrait le faire.


EDIT

Celà va sans dire toutefois c'est mieux en le disant:
Si on écrit (x:One) |-f-> f x on ne pourra écrire aucun énoncé bien typé qui affirmerait une propriété de f. Pourquoi? Parce qu'une fonction récursive est l'implémentation d'un raisonnement par récurrence. Le raisonnement inductif doit rester acyclique.

1. Ne pas pouvoir prouver n'interdira pas d'écrire
2. Le fait d'écrire ne garantira pas que l'on puisse prouver sans modifier le code
3. Si on a l'intention de prouver un énoncé alors il existe une façon raisonnable de l'implémenter sans modifier le code
4. D'une façon générale il n'existe pas de façon raisonnable de prouver des énoncés raisonnables