Mon Jean-Raymond par Dominique Cansell

 Mon Jean-Raymond
Dominique Cansell (Lessy)
dominique.cansell@gmail.com

 

Jean-Raymond n’est pas à moi. Il est à tout le monde. Si j’emploie ”mon” c’est parce que ce texte est
aussi mon histoire, mon histoire autour des travaux communs avec ceux de Jean-Raymond. Je vous prie de m’excuser. Ce n’est pas un texte scientifique. Le lecteur pourra facilement trouver les papiers dont je parle dans ce document.
     J’ai eu extrêmement de chance de le rencontrer et surtout de travailler avec lui. Je n’étais pas vraiment prédestiné à le rencontrer. À Metz je fais peu de recherche et j’enseigne l’algorithmique en utilisant la preuve très tôt avec une importance pour l’algorithmique récursive. Par contre, je ne le savais pas encore, j’avais le bagage mathématique pour faire les preuves en B.
     En 1997 je décide de rejoindre l’équipe de Dominique Méry à Nancy. Je ne travaille pas directement sur B. Comme B n’était pas un langage récursif (je ne connaissais pas les méthodes) j’avais décidé bêtement de ne pas l’utiliser. Par contre j’utilise le Logic-Solver un langage utilisé par l’AtelierB. Je téléphone quelquefois(mais rarement) à Jean-Raymond pour avoir des conseils.
     Début 1998 Jean-Raymond vient faire un exposé au LORIA sur son prouveur de prédicats (pp) développé en Logic-Solver pour prouver les règles du prouveur de l’AtelierB. Durant l’été 1998 je veux apprendre la programmation orientée objet et je prends pp comme programme à développer. À la conférence AFADL en 98 je parle de mon programme à Jean-Raymond. Il vient d’emménager à Marseille mais me propose d’en parler plus en détail et de lui faire une démo à Paris dans le bureau de Véronique Donzeau-Gouge au CNAM (Conservatoire National des Arts et Métiers).
     Je ne faisais toujours pas de B en recherche mais j’avais décidé de l’enseigner à Metz et en DEA à Nancy avec l’AtelierB. Pour cela je devais m’entrainer à utiliser le prouveur interactif de l’AtelierB. Ce n’était pas simple au début. On ne savait pas toujours où on se trouvait dans la preuve. On peut comprendre que beaucoup aient abandonné. C’est pour apprendre aux étudiants que j’ai appris moi-même. Le seul secret pour aider le prouveur c’est de savoir faire des preuves. Je commençais à beaucoup utiliser pp lors de la preuve interactive.
J’ai aussi fait mes premiers développements B entièrement prouvés.
     En 2000 je suis allé à Marseille avec Dominique Méry où j’ai montré à Jean-Raymond comment j’utilisais pp dans la preuve interactive et lui nous a montré son développement de l’agent mobile (Luc Moreau). Je l’ai directement enseigné en DEA en septembre. Notre collaboration a dû commencer là.
     Dominique Méry nous propose de développer le protocole d’élection d’un leader (IEEE 1394). Travailler avec Jean-Raymond est très dur car il faut aller vite sinon il fait le travail rapidement tout seul. Pour être honnête, même si j’ai fait quelques preuves sur les arbres, j’avoue avoir été un peu à la traıne.
      Puis je reçois une lettre manuscrite de Jean-Raymond avec entre autre la preuve du théorème de Zermelo(son travail avec Guy Laffitte). Quatre jours après les modèles étaient entièrement prouvés avec l’AtelierB.
      Jean-Raymond couchait ses preuves sur papier avant de passer à l’outil
      Après toutes ces preuves, Jean-Raymond me demande de travailler sur l’interface du prouveur interactif pour démocratiser l’activité de preuve. Ce développement (en Xemacs pour l’interface et le Logic-Solver) nous a pris beaucoup de temps (écriture du programme) et, en plus de nos nombreux échanges (emails, téléphone) je descendais au moins une fois par mois à Marseille pour faire le point. Click’n Prove (ou la Balbulette) a été beaucoup utilisé par nous deux, les chercheurs et les étudiants avant que Rodin ne soit développé.
      Fin 2001 je demande à Jean-Raymond de participer à la journée à Nancy consacrée à la méthode B
(27/02/2022). Il refuse car on lui a enlevé son cours à l’école des jeunes chercheurs du CNRS. Cela l’a
beaucoup affecté. J’ai beaucoup insisté et à la fin je lui ai dit que lui seul pouvait parler de B et diffuser ses idées. Il a fini par accepter. Ouf.
      Pour tous nos développements nous commencions à introduire les nouveaux événements concrets dans l’abstraction pour dire qu’ils respectent l’invariant et font décroitre un variant pour que les obligations de preuve Event-B soient générées par l’AtelierB et ces travaux ont conduit à notre papier ”Refinement and Reachability in Event-B”
      En 2004 Jean-Raymond me demande de le suivre à Zürich. Je refuse car je ne veux pas laisser ma
famille sans moi mais je fais beaucoup de preuves avec Click’n Prove pour certifier des règles du prouveur interactif de Rodin. Jean-Raymond m’y invite au moins deux fois. La deuxième fois nous avons travaillé sur l’algorithme ”4-slots” de Simpson (travail publié dans son dernier livre sur Event-B). Nous faisons encore nos dévelopements avec Click’n Prove jusqu’à la fin 2006 ou début 2007. Après nous n’utilisions que Rodin que j’utilisais déjà avec mes étudiants.
      En 2008 je décide d’arrêter officiellement ma recherche (en conflit avec l’université et la politique de la direction de l’Inria, aux niveaux local et national qui ne m’a pas soutenu) cela ne valait plus le coup de s’investir. Par contre j’ai toujours gardé le contact avec Jean-Raymond (ou alors le contraire). J’ai passé beaucoup de temps à relire son livre sur Event-B avant sa publication en 2010.
      Lorsqu’il est revenu à Marseille, j’y allais pour le voir et discuter de nos développements et preuves
respectifs. Nous n’avions pas de projet commun.
      En 2017 Jean-Raymond travaille sur la séquence de Goodstein. Il avait réussi à prouver la version faible mais était bloqué sur la vraie séquence de Goodstein où il faut des ordinaux. Il me demande de l’aider. Jean-Raymond pensait pouvoir faire la preuve avec Peano (récurrence sur les naturels). Il avait presque une preuve qui me semblait aussi correcte mais Rodin n’était pas d’accord. Nous avons failli arrêter plusieurs fois jusqu’à trouver la bonne structure (en fait des ordinaux sans le savoir) qui nous a permis de finir la preuve.
      Fin 2018 il a pris une grande décision: il va déméngager le 1er janvier 2019 pour une résidence sénior car il a maintenant des difficultés pour monter les quatre étages avec ses mauvaises jambes. Il me dit qu’il y a des possibilités pour avoir des invités À bon entendeur!
      En 2019 Jean-Raymond m’envoie son modèle direct d’un protocole (variante du Paxos de Leslie Lamport). Il était désespéré: il n’arrivait toujours pas à mettre en place les bons invariants pour prouver formellement le protocole Paxos de base. Nous avons mis trop de temps pour trouver le dernier invariant et nous avons failli abandonner souvent. Lorsque j’ai trouvé et prouvé le dernier invariant (le 19 décembre 2019) j’ai rendu Jean-Raymond heureux.
      En 2020 Jean-Raymond a commencé à écrire notre papier sur le Paxos. Il prenait plus de temps que
d’habitude. Pour la première fois je lui ai écrit des parties avec les explications en français ainsi que les
modèles Event-B (événements et invariant). Pendant cette période il y avait aussi la pandémie comme il était souvent seul je lui envoyais des photos des fleurs, plantées par Isabelle, de notre jardin. J’ai appris après son décès qu’il en avait partagées avec ses proches.
     Fin 2020 Jean-Raymond me demande de participer à son instanciation de contextes Rodin pour faire des mathématiques dans le cadre du projet ANR EBRP. J’ai d’abord refusé car je ne voulais plus travailler avec d’autres que Jean-Raymond mais comme sa santé commençait à se dégrader j’ai accepté. Ce fût une période passionnante pour moi mais Jean-Raymond ne pouvait hélas plus se concentrer longtemps.
     Je suis allé le voir deux fois en 2022 pour lui montrer le travail qu’il m’avait demandé de faire. Il m’a annoncé qu’en 10 ans nous avions échangé plus de 6000 emails (sans ceux du LORIA ). Il m’a aussi demandé de répondre à des emails sur B de collègues. Je lui ai proposé de le promener avec son fauteuil. C’est durant ces promenades que j’ai prise mes deux dernières (et premières) photos de Jean–Raymond. Il m’a dit que c’était la première fois qu’il sortait de la résidence depuis qu’il était en fauteuil sauf pour des visites médicales. Il était pudique et ne voulait pas imposer son handicap à d’autres. C’était sa volonté. Il m’a également donné son vieux mac. Il ne m’a pas vraiment dit pourquoi. Il a dit prends le. Je pense que c’est parce qu’il contenait nos fichiers latex. Je m’en suis rendu compte lorsque je dus compléter ses travaux sur les réels et notre protocole ”Paxos”. D’ailleurs j’écris ce texte sur son mac.
     Nous avons encore échangé longtemps par email et téléphone mais Jean-Raymond était très fatigué et ne pouvait plus tenir une conversation soutenue. Ses conseils par emails étaient encore judicieux. Il n’a jamais perdu sa tête. En décembre 2024 j’avais écrit un papier sur son instanciation. J’avais mis son nom dans le titre mais il m’a demandé de l’enlever. Au début 2025 je l’ai eu au téléphone un peu plus longtemps, sa voix était bien meilleure et ses problèmes à la maison senior étaient réglés. Je me suis dit super je pourrai le revoir cet été.
     Son dernier email c’était le 18 février pour me dire qu’il y avait encore du pain sur la planche. Il avait lu dans le Monde (qu’il lisait tous les jours) que des mathématiciens allaient prouver avec Lean le théorème de Fermat. Son dernier sms date du 24 mars 2025 pour me dire qu’il avait déjà vu Irlande-France en rugby féminin et que ce n’était pas la peine de lui envoyer un lien pour le résumé du match. Il adorait le rugby.
     Je lui ai encore envoyé des sms ou mms après son décès. Le dernier c’était une photo d’une règle à calcul circulaire pour lui demander s’il la connaissait.
     Jean-Raymond avait aussi beaucoup d’invariants dans sa vie: beaucoup d’escaliers, même restaurant
(jusqu’à ce qu’il ferme définitivement), même repas (saucisson et pâtes). Pour atteindre son appartement à Marseille il fallait grimper les quatre étages (cinq à Zürich), ensuite après un bon café, Jean-Raymond écrivait sur des feuilles le planning des objectifs à atteindre pour ma visite. À la fin il raturait ce qui avait été fait puis déchirait les feuilles content du travail accompli. Jean-Raymond était aussi un grand marcheur et un grand grimpeur. Je me souviens (en 2002) de petites escalades dans les Calanques avec lui et Christophe Metayer et surtout d’une longue marche dans les Calanques avec lui et Ralph Back. Il fallait le suivre, il nous avait épuisé. C’était un très bon skieur et un passionné des déserts et quand il y était j’étais en vacances pas d’email ni de téléphone. D’autres en parleront sans doute mieux que moi.
     Jean-Raymond était un orateur hors pair qui prenait beaucoup de temps pour préparer ses présentations.
On avait toujours l’impression que c’était simple et limpide. Lors des journées que j’ai organisées il y avait toujours beaucoup de monde pour l’écouter et les gens venaient à Nancy de loin. Il adorait aussi transmettre et côtoyer les jeunes comme à l’école des jeunes chercheurs, à Zürich et dernièrement à Shanghai. Il formait ses étudiants à la preuve en utilisant Rodin et en limitant les règles automatique du prouveur. Li Qin en parlera sans doute mieux que moi.
     Il aimait beaucoup la danse. En 2016 j’avais vu un spectacle de Luc Petton avec ses grues de Mand-
chourie. Il voulait absolument le voir. Par chance un mois plus tard ce spectacle arrive à Marseille. Il y est allé avec une cousine. Éblouissant a-t-il dit. Pendant la pandémie je lui ai envoyé des liens vers des spectacles de Béjart et d’autres.
     Jean-Raymond adorait la peinture comme celle de Fernand Leger, celle de Braque (il produisait moins que Picasso mais c’est pour lui d’une grande qualité), celle de Klimt (qu’il a été admirer à Wien en 2014) et surtout celle de Vemeer. En 2015 il est allé à Dresde où il a eu le plaisir d’admirer deux Vemeer, dont ”la jeune femme lisant une lettre à la fenêtre”. En 2017 à Franckfort il a vu le Géographe au musée Städel. Il a vu une grosse dizaine de Vermeer sur les 35 connus. Son regret est d’avoir loupé l’exposition Vermeer et les maıitres de la peinture du genre au Louvre.
     En 2009 nous sommes allés au centre Pompidou Metz pour voir ensemble la première exposition: Chefs-d’œuvre. À chacune de mes visites de musée je lui envoyais des photos des expositions comme celle de de Fernand Leger en 2017, celle de Braque en 2019 à Rouen et beaucoup d’autres.
     Jean-Raymond était très discret. Je ne sais pas s’il cloisonnait en ne me parlant pas de ses anciens travaux (sauf sur B) et collègues et/ou les gens qui ne l’aimaient pas. Je pense que pour les premiers il ne se retournait pas et allait de l’avant sans oublier pour les deuxièmes il était comme cela et c’était sans doute aussi pour me protéger. En fait je ne connaissais qu’une partie émergée de Jean-Raymond. En lisant les hommages qui lui sont consacrés j’ai découvert la partie émergée. Je remercie Nora, sa femme de ménage, de s’être occupé de lui jusqu’à la fin.
     Le 18 juin je suis allé à Dougne dans le Tarn pour voir la tombe où seront déposées ses cendres. Ne
sachant quoi faire j’y ai dessiné un B avec des cônes d’un cyprès du cimetière. Au revoir Jean-Raymond.

C’était un réel plaisir de travailler avec toi. Merci.

    Mes deux photos de Jean-Raymond et mon B à Dourgne

Chapeau Jean-Raymond !