Discussion :

[Steki-kun]

Après, c'est toujours pareil... Il faut faire un choix entre expressivité et utilisabilité. Autant annoter son code avec des pré et post conditions et quelques invariants de boucle, on peut espérer qu'un jour les programmeurs le feront, autant faire des preuves dans le CCI, il ne faut pas se leurer, seul un petit nombre de cinglés joueront avec ça ! Mais il y a toujours une volonté des cinglés en question de travailler sur des outils prouvant statiquement les codes annotés par des gens "normaux" (quitte à prouver la validité de ces outils en Coq justement), donc tout n'est pas perdu :-)

Non mais dis donc, ça marche très bien d'abord (et en plus c'est très amusant ), bon d'accord c'est pas pour tout le monde mais on s'y attèle

Steki le cinglé

[alex_pi]

Non mais dis donc, ça marche très bien d'abord (et en plus c'est très amusant ), bon d'accord c'est pas pour tout le monde mais on s'y attèle

Steki le cinglé

Nan mais tu sais bien que moi aussi ça m'ammuse, et que je suis raisonnablement convaincu de l'utilité et de la puissance intrinsèque de la chose hein C'est juste que je suis aussi raisonnablement convaincu que c'est completement inutilisable pour 99,9% des gens quoi :-)

[Steki-kun]

Héhé j'en suis bien conscient mais je me sentais visé Disons que j'aime voir ce problème ainsi : tu aurais pu écrire la même chose en parlant du simple fait d'écrire un programme, il y a un peu plus de 50 ans. Certes les machines étaient rares, mais le fait même d'écrire du code machine sur papier, puis de le perforer sur cartes, rendait la chose assez tordue Ca devait être difficile à l'époque de s'imaginer que l'activité de programmation deviendrait si répandue, et même qu'on pourrait écrire des systèmes très complexes de cette manière.
Tout ça est devenu possible parce que des pionniers en ont chié à développer des langages de plus haut niveau, des compilateurs qui faisaient le travail chiant à notre place, des systèmes de types, etc... J'ose croire que dans le futur, les systèmes de preuves de prog à la Why ou à la Boogie seront intégrés avec les langages concernés (ou au moins dans les IDE, comme c'est presque déjà le cas avec Boogie et C# en fait), que la preuve automatique aura fait bcp de progrès etc, que la preuve interactive aussi (parce qu'on aura tjs besoin d'intervention humaine dans certaines preuves de tte façon) de telle sorte que la correction d'un programme soit partie intégrante de son design pour une grande partie des programmeurs
Il faut bien rêver un peu d'abord, et puis surtout il faut une raison pour se lever le matin

[InOCamlWeTrust]

Ton credo, c'est un peu le United Colours of Developpez.com, non ?

Les systèmes de preuve évolueront, mais je ne pense pas un seul instant qu'ils seront utilisés systématiquement par tout le monde un jour ou l'autre... tout simplement parce que tou le monde n'a pas besoin de système de preuve !

I faudrait à mon sens, revenir en informatique à un certain "bon sens de la programmation", et arrêter de se branler avec des générateurs automatiques de je-sais-pas-quoi, des systèmes de personne-ne-sait-pas-trop-quoi, et tout ce genre de trucs.

Très certainement tout ça c'est très beau, ça peut servir dans certains cas particuliers, mais ça ne crée aucune valeur ni pour l'utilisateur (combien d'heures pour apprendre tel logiciel qui fait un peu n'import quoi), ni pour le client final.

Le must, dans le genre, c'est SAP : un bon truc à foutre à la Corbeille. Peu flexible, lourd, cher (très !!!), et surtout une chose qui, soti de l'emballage, ne sait rien faire, car étant "générique", one peut tout faire avec du moment qu'on crée le mdule... Heureusement pour eux que les gens qui décident de son installation dans les entreprises n'y connaissent rien à l'nformatique (ou presque) !

Il faudrait arrêter de faire de l'informatique pour informaticiens, un peu.

Dommage que ça ne se brûle pas les logiciels et les programmes !

Allumons les feux de joie
Que les flammes purificatrices
Brillent du plus fort éclat
Et ne soignent à jamais nos cicatrices

[alex_pi]

@Steki-kun
Oui, mais les gens se servent d'un compilo sans en connaitre le fonctionnement, des systèmes de types sans en comprendre la théorie, et des langages de programmation sans notion de sémantique oppérationnelle à petit pas ! Donc autant je veux bien croire que des outils comme Krakatoa ou Caduceus ont un avenir "grand public", autant j'ai de gros doute pour Coq. Je veux bien croire que des gens accepterons qu'on leur dise que leurs pré et post condition ont été prouvées par Ergo, mais je ne pense pas qu'ils se pencheront sur son solveur. Et ces outils sont utilisable sans en comprendre la théorie. Je ne pense pas que ce soit le cas de Coq. Et donc il ne sera pas utilisé par le "grand public". Ce qui ne m'empeche pas, une fois de plus, de croire en la puissance de Coq, ni à son utilité effective, mais dans des cas extremement spécialisé, comme l'écriture d'un compilateur C certifié, ou un système javacard.
Bref, pour moi il y a un monde entre un système (même formel et complet) de design par contrat, et le calcul des constructions inductives.

[alex_pi]

Il faudrait arrêter de faire de l'informatique pour informaticiens, un peu.

Et bien justement... Le jour où on fera *pour de bon* des programmes fiables, peut être que l'informatique sera effectivement accessible aux non informaticiens !
Dans le monde réel, si tu achete un mixeur, que tu rentres chez toi, et que le bouton "mixer" ne fonctionne pas, tu le rapportes au magasin, et tu gueules pour en avoir un neuf. Dans le monde informatique, quand un programme ne marche pas, les gens acceptent de passer des heures à chercher sur les forums comment le faire fonctionner. Quand un traitement de texte crash parce qu'on a cliqué trop vite sur deux boutons, on se dit que ça nous apprendra à ne pas avoir sauvegardé toutes les 5 minutes. L'informatique est un domaine où il semble normal d'avoir des produits mal finis, qui bugent à tout va, etc.

Et puis de toutes façons, autant il est normal qu'un système d'exploitation ai pour but d'être accessible à tous, autant je ne vois pas pourquoi un langage ne pourrait pas être réservé aux "informaticiens". Il me semble assez raisonnable de faire des langages et des outils qui gravitent autour (comme des langages d'annotation) en les pensant pour les informaticiens et non pour madame Michu.

Après, encore une fois, je ne pense pas que Coq soit addaptés à grand monde, et ce n'est bien sûr à utiliser que lorsque l'ont veut avoir un grand degré de sûreté, pas pour développer un traitement de texte. Mais les annotations à la JML, je ne vois pas pourquoi il faudrait s'en priver, et les prouveurs automatiques à partir d'annotations font des progrès très intéressants.

[Steki-kun]

Le "oui mais" qui débute ton post est superflu, je ne vois pas en quoi il s'oppose à ce que j'ai écrit ! Je n'ai pas écrit que Coq deviendrait facile à utiliser et répandu, mais que le travail que l'on fait de nos jours sur ces outils exotiques est justifié par le fait qu'il pourra rendre les méthodes formelles accessibles à plus de gens dans l'avenir, et par méthodes formelles je n'entends pas développer son programme dans le CIC, mais plutôt annoter son code et utiliser Caduceus + un prouveur automatique certifié (Ergo ça me va ^^) + idéalement un système de preuve interactif qui reste à imaginer et qui permette à l'utilisateur d'aider le prouveur automatique lorsque tout n'est pas déchargé automatiquement. Rendre ce processus et ces outils plus faciles à appréhender est le vrai enjeu à mon avis. Et je suis persuadé qu'on est d'accord en fait

Après, en amont, il faut tjs des spécialistes qui fassent des trucs qu'eux seuls comprennent et que les autres utilisent, mais c'est vrai en toute chose et à tout niveau, et n'en déplaisent à certains c'est gratifiant

[alex_pi]

Et je suis persuadé qu'on est d'accord en fait

Oui