Re: Et pendant ce temps, CamlLight poursuite sa route...

Mea culpa, je reconnais avoir été un peu sec dans mes réponses ce qui est un manque évident aux régles de bienséance, j'en suis désolé.

L'erreur est humaine, l'entêtement est diabolique (errare humanum est, perseverare diabolicum comme disent les latinistes), quelque soit le point sur lequel l'on se trouve pris en faute. Peu importe les torts réspéctifs de chacune des parties, l'important est la conciliation ou la réconciliation.

À l'origine de cette controverse, dispute ou discussion (choisis le mot qui te convient, peu m'importe) il y a effectivement, semble-t-il, une méprise. Je n'ai jamais, mais alors jamais, voulu dénigrer l'approche pragmatique par tests unitaires mais la critiquer, implicitement, cela est certain : mais la critique qui consiste à exposer les limites d'une méthode (ce qui sera à jamais en dehors de sa porté, et quand je dis jamais ce n'est pas parce que l'on ne sait pas faire aujourd'hui, mais parce l'on ne saura jamais faire certaine chose avec cette méthode, comme dans le théorème de Rice par exemple ;-) ne signifie pas le dénigrement (c'est nul, ça ne sert à rien et autres joyeusetés).

La pratique des tests unitaires est indispensable, comme approche, pour essayer de garantir le mieux que l'on peut que les programmes que l'on fait tourner sont corrects, dans la quasi-totalité des langage de programmation, et en OCaml particulièrement. Je n'aurai certainement pas contribuer à la rédaction de cette dépêche (la partie sur les améliorations du compilateur, avec chicco) si je considérai que la nécessité de reccourir à des tests unitaires en faisait un langage bon à mettre à la poubelle. ;-)

Le recours à des méthodes plus strictes et formelles pour garantir, avec certitude, qu'un code (ou un circuit) satisfait à ses spécifications n'est pas la panacée. Mais, contrairement à ce que tu crois, elles sont loin d'être un échec : et cela non uniquement dans les labarotoires de recherches, mais elles sont utilisées dans l'industrie depuis plus de vingt ans ! ;-) Et ce n'est pas le nombre d'acteurs industriels qui manquent : il me semblait avoir donné une liste importante dans ce message (et pas des moindres : IBM, Intel, Nasa, Agence Spatiale Européenne, Airbus...).

Pour te faire une meilleure idée de mes considérations sur les langages en informatique, je te propose la vidéo de cette conférence que j'avais abordée dans ma discussion avec chimrod.

Je me sens dans l'obligation de teaser un peu en commençant par sa conclusion : « j'espère avoir démonté l'idée qu'un langage est mieux que les autres, il y'en a qui sont moins bien que les autres ça c'est vrai, mais il n'y en pas qui sont mieux, il y a des choses différentes » (ce que j'exprimais, à ma façon, dans ce message en disant qu'il faut choisir l'outil adapté à ses besoins, ce qui nécessite de bien connaître ses besoins ainsi que les outils disponibles, leur qualités et leur faiblesses).

Il y a tout un passage tout à fait juste et assez comique sur les guerres de religion entre langage, dont voici la transcription de quelques diapos qu'il utilise :

L'imprératif

Détracteurs : l'impératif c'est un nid à bug, en particulier à cause des pointeurs et de la gestion mémoire par les utilisateurs

Partisans : Mais non, la programmation y est très naturelle, et il suffit d'y ajouter les assertions, les contrats, l'analyse statique, etc.

Le fonctionnel

Détracteurs : le fonctionnel, c'est pour les intellos, et c'est inefficace

Partisans : Mais non, ça demande juste un peu de culture scientifique, et l'inneficacité c'est du passé ! Le typage fort et la gestion automatique de la mémoire donne de la sécurité. Et on peut bien mieux raisonner sur les programmes, voire les prouver [là c'est moi qui graisse].

L'orienté objet

Détracteurs : L'objet c'est la fausse bonne idée : ça a l'air bien au début, mais il y a plein de problèmes (ex. héritage multiple) et c'est super-verbeux !

Partisans : Mais non ! l'héritage simple suffit le plus souvent, la programmation est naturelle et proche de l'architecture, elle passe bien à l'échelle, et le résultat est très efficace

La programmation logique qui a toujours était marginale

Détracteurs : La programmation logique et les contraintes, c'est bien joli, mais on ne sait jamais si ça va marcher et combien de temps ça va prendre !

Partisans (il précise « argument massue » dans la vidéo): Causez toujours, vous ne savez absolument pas faire ce que nous faisons !

Après avoir abordé les différents paradigmes, les principes du typage (dynamique ou statique) il conclue sur ces deux diapos :

Typage et vérification formelle

• Typage dynamique : arrêter l'éxécution en cas de d'opération illégale (choux + carotte)—Scheme, Python, etc.

• Typage Statique : dès la compilation, classifier les expressions selon les valeurs dénotées, et assurer la compatibilité des arguments des opérations

• Vérification formelle : dès la compilation vérifier des propriétés quelconques (cf. séminaire de T. Jensen) [NdM : séminaire qui suit le sien, où T. Jensen présente essentiellement un système d'annotations ajouter dans les commentaires de code Java, ce que gasche a présenté comme solution par invariants et préconditions]

Que peut-on savoir sur le programme sans l'exécuter, et à quel prix ?
Intuition : le typage doit être très rapide

À l'oral, comme commentaire à la question centrale de la diapo, il ajoute « et ça quand on fait des avions c'est assez utile. S'il fallait débuguer les avions en les crachants [NdM : approche tests unitaires] ce serait moyen comme idée, mais on le fait un peu sur les bagnoles » (se souvenir de Airbus dans la liste des industriels ;-)

Et celle-là qui classifie les niveaux et différents systèmes de typage

Niveaux de typage

1. Interdire choux+carottes
2. Typer les fonctions et leurs applications : C, Java, etc.
3. Typer l'ordre supérieur (fonctions de fonctions)
4. Accpeter les types polymorphes (paramétriques)
5. Sous-typage (langage objets)
6. Inférence de types : trouver les bons types même lorsqu'ils ne sont pas écrits par le programmeur
7. Typage de modules et APIs : Programming in the large
8. Niveau maximal actuel : Coq, cf. cours du 18 mars 2015, types dépendants, typage garantissant la terminaison, mais l'inférence générale n'est plus décidable

Enfin, plus tôt dans sa conférence, il fait une allusion au langage B et B-event de Jean-Raymond Abrial qui les a utilisé pour certifier du code pour la RATP dans les années 90 (en l'occurrence, ceux qui empreintes la ligne 14, en tête là où il n'y a pas de chauffeurs et où on voit devant soit, il y a un ordinateur qui fait tourner du code B ;-).

Et M. Abrial avait présenté cette histoire en 2015 dans cette conférence dont voici le texte de présentation :

Cette présentation est celle d’un chercheur vieillissant qui porte un regard historique sur les trente dernières années de son travail.

Il y a deux sortes de chercheurs : les prolifiques et les monomaniaques. Je fais partie de la seconde catégorie, car j'ai toujours pratiqué le même genre d’investigations, à savoir la spécification et la construction vérifiée de systèmes informatisés.

Ce travail, autant théorique que pratique, s’est concrétisé au cours de toutes ces années dans trois formalismes voisins : Z, B et Event-B (dont je ne suis pas, loin de là, le seul contributeur). Je vais tenter d’expliciter comment les idées que contiennent ces formalismes et les outils correspondants ont lentement émergés de façon parfois erratique.

Je tenterai aussi de préciser les multiples influences qui ont participé à cette évolution. En particulier, je montrerai comment plusieurs réalisations industrielles ont permis de progresser dans ce domaine. Mais je soulignerai aussi les échecs et parfois les rejets de la part de communautés tant universitaires qu’industrielles.

Pour finir, je proposerai quelques réflexions et approches pour le financement de recherches telles que celle-ci.

J'en extrairai juste trois diapositives :

la première en plein dans le sujet de la discussion

la RATP décide de supprimer les tests unitaires et d'intégration

Octobre 98 : lancement de la ligne 14

Depuis lors pas de problèmes avec le logiciel développé avec [soit 17 ans plus tard, et il tourne, tourne, tourne...]

pour remplacer la démarche par

86.000 lignes en ADA ont été produites automatiquement

27.800 preuves ont été faites

92% ont été prouvés automatiquement par l'Atelier B

Coût des preuves interactives : 7 hommes-mois

Les preuves interactives sont moins chères que les tests

Conséquence de cette première historique (date d'ouverture en 1998, rappelons-le, donc je te laisse imaginer depuis quand les ingénieurs utilisaient ces outils ;-)

Métros utilsant B pour leurs développements : New York City, Amérique du Sud, Europe, Chine, etc.

Projets plus récents en France avec B :

• Ligne 1 de la RATP à Paris (sans conducteur)

• Navette de l'Aéroport Charles de Gaulle (sans conducteurs, 158.000 lignes en ADA, 43.600 preuves, 96.7% auto)

J'espère avoir montré que ces méthodes de certification formelles (en grande partie automatisée) sont loin d'être un « échec », et t'avoir donné envie (ainsi qu'à d'autres) d'aller jeter un œil sur ces deux conférences.

Pour conclure, je citerai un extrait du message de Dinosaure et y avoir en partie satisfait :

Le deuxième point est ton apprentissage individuel. Les personnes qui composent la communauté OCaml sont souvent des chercheurs qui ont un savoir assez impressionnant (et qui dépasse souvent le simple cadre de la communauté OCaml) se qui fait qu'il est toujours intéressant de discuter avec ces personnes qui vont te pointer vers des documents qui t'en apprendront plus sur les langages informatiques (domaine de prédilection d'OCaml), les algorithme et les paradigmes. L'avantage est qu'on garde toujours une réalité de ces connaissances qu'on peut appliquer (et qu'on applique) dans l'industrie. Ce qui fait que même si la courbe d'apprentissage est rude, elle n'en est pas moins impossible - par exemple, je viens tout droit d'un milieu très industriel (et j'ai ignoré presque tout les aspects théoriques de l'informatique) et pourtant j'arrive à m'en sortir en comprenant des concepts que je n'aurais jamais eu la chance de voir dans le milieu d'où je viens.

Il est vrai que les chercheurs (ou ceux qui ont des connaissances approchantes) aiment bien aider, même s'ils peuvent se montrer susceptibles ou soupe au lait quand ils ont l'impression que l'on cherche à leur expliquer des principes théoriques qu'ils connaissent bien et considèrent comme triviaux.

Sur ce, j'espère qu'après ces échanges nous nous quitterons bons amis. :-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.