Ce qu’il faut savoir sur les compilateurs et leur vérification (2/2)

Sandrine Blazy, Professeure à l’université de Rennes et directrice adjointe de l’IRISA, est une spécialiste des compilateurs et des logiciels sûrs. Elle a développé avec Xavier Leroy, CompCert, le premier compilateur pour le langage C vérifié à l’aide de Coq. Pour ce véritable tour de force scientifique et technique, elle a obtenu la médaille d’argent du CNRS (une des plus belles récompenses scientifiques en France). Si vous ne comprenez pas en quoi cela consiste, Sandrine va l’expliquer à binaire et ce sera l’occasion d’un peu mieux comprendre ce qui se passe dans un ordinateur. Serge Abiteboul et Pierre Paradinas

Deuxième partie de l’article.

© Jean-Claude MOSCHETTI / IRISA / CNRS Images

La sémantique de ces langages et la vérification déductive

Dès l’invention des premiers langages de programmation, s’est posée la question de savoir comment définir précisément un langage, c’est-à-dire comment décrire le comportement de tout programme. Une première réponse pragmatique a été de considérer qu’un langage est défini par son compilateur (compiler le programme pour l’exécuter ensuite et observer certains de ses comportements). Une seconde réponse est venue à nouveau des mathématiques, cette fois-ci de la logique mathématique. En effet, indépendamment du développement des premiers ordinateurs, des logiciens ont proposé des théories des langages de programmation, focalisées sur des langages de programmation théoriques, comme le lambda calcul de Church (1930), dont les principes seront par la suite mis en œuvre dans les langages de programmation fonctionnelle. Ainsi sont apparus les formalismes fondamentaux caractérisant un langage de programmation, notamment la syntaxe, la sémantique formelle (caractériser sans ambiguïté le comportement attendu de tout programme, quelles que soient ses valeurs fournies en entrée) et ses différents styles, et les principes de raisonnement déductif associés. Ces formalismes sont toujours l’objet de recherches actives.

Un de ces styles sémantiques est à l’origine de la vérification déductive, qui permet d’avoir des garanties très fortes sur l’absence d’erreurs dans les logiciels. Cela été l’occasion de revisiter et pousser plus loin les premières intuitions de Turing lorsqu’il avait démontré la correction de son organigramme. La vérification déductive permet de démontrer mathématiquement la correction d’un logiciel, c’est-à-dire qu’il satisfait sa spécification, écrite dans un langage logique pour éviter toute ambiguïté du langage humain. Aujourd’hui, grâce à la vérification déductive, on dispose de logiciels vérifiés, constitués d’un logiciel et d’une preuve de sa correction, qu’on peut rejouer ou fournir à un tiers de confiance. Cette preuve nécessite de raisonner sur des propriétés du langage dans lequel est écrit le logiciel, en particulier sur la sémantique formelle de ce langage.

Avec des langages réalistes, le raisonnement ne peut plus se faire à la main, mais il nécessite d’être automatisé par des outils logiciels d’aide à la preuve. Les premiers de ces outils sont apparus au début des années 70. De même que les premières machines ont été conçues pour mécaniser la résolution d’équations, les sémantiques formelles et la logique ont permis de mécaniser le raisonnement déductif sur les programmes, et donc de développer les outils logiciels automatisant les idées issues des intuitions de la fin des années 60. Ces outils ont beaucoup progressé ces dernières années. Ils se regroupent en deux familles :

      1. les logiciels de preuve automatique, qui prennent en charge la totalité d’une preuve, en déchargeant les formules logiques à prouver vers des solveurs de logique capables de déterminer si ces formules sont vraies ou fausses; et
      2. les assistants à la preuve, des logiciels qui permettent de mener une preuve mathématique vérifiée par ordinateur, c’est-à-dire une démonstration en interaction avec l’assistant de preuve, au moyen de commandes indiquant comment progresser. L’assistant de preuve automatise une partie du raisonnement, s’assure que la démonstration est complète et respecte les lois de la logique mathématique, alors que l’utilisateur décide comment raisonner et progresser dans le raisonnement.

Mener une preuve de correction est une activité à part entière, qui nécessite d’inventer puis établir les invariants (sémantiques) du logiciel, qui sont des assertions devant être garanties à tout moment de l’exécution du programme. Cela peut nécessiter de définir les principes de raisonnement associés. Le programme “majorité” (Boyer, Moore, 1980) déterminant de façon efficace le candidat majoritaire (i.e., qui remporte une élection à scrutin majoritaire) d’un ensemble de bulletins de vote en est une illustration. Le programme est surprenant de par sa simplicité, mais sa compréhension demande à réfléchir à son invariant qui est difficile à trouver, car cela nécessite d’imaginer un arrangement des bulletins de vote, qui n’est pas calculé par le programme. On se retrouve ainsi dans le cas plus général où il est nécessaire d’inventer pour les besoins de la preuve une structure de données qui n’est pas utile au programme.

Retournons au début des années 70. Le premier programme dont la preuve a été mécanisée est un compilateur rudimentaire d’un langage d’expressions arithmétiques (Milner, 1972, LCF). Un compilateur était un exemple représentatif d’un programme particulièrement complexe. Le théorème de correction d’un compilateur exprime que le code produit doit s’exécuter comme prescrit par la sémantique du programme source dont il est issu. C’est une propriété de préservation sémantique, qui devient mathématiquement précise dès lors qu’on dispose de sémantiques formelles (pour les langages source et cible du compilateur). Ici, il devient : pour toute expression, sa valeur calculée par la sémantique du langage source est exactement la valeur renvoyée par l’exécution du code de l’expression compilée. Ce théorème est établi une seule fois, pour toute expression donnée en entrée au compilateur. Désormais, la vérification de ce petit compilateur jouet de 1972 est enseignée à titre d’exercice dans des cours de master.

Aujourd’hui, le compilateur demeure un logiciel particulièrement complexe (de par les nombreuses optimisations qu’il effectue afin de produire du code efficace), mais également le point de passage obligé dans la chaîne de production du logiciel. Aussi, le vérifier permet de s’assurer qu’aucune erreur n’est introduite lors de la compilation, et de préserver les garanties obtenues au niveau source sur le logiciel. L’idée d’avoir un théorème unique démontré une fois pour toutes, ainsi qu’une preuve lisible était déjà présente en 1972, mais il a fallu attendre plusieurs dizaines d’années pour que la compilation vérifiée se développe et passe à l’échelle.

Diagram of the CompCert compiler

CompCert est le premier compilateur optimisant ciblant plusieurs architectures et utilisé dans l’industrie, qui soit doté d’une preuve mathématique de correction vérifiée par ordinateur. Cette preuve a été menée avec l’assistant à la preuve Coq. C’est un compilateur modérément optimisant du langage C, le langage le plus utilisé dans l’industrie pour programmer des logiciels embarqués critiques, dont le mauvais comportement peut avoir des conséquences catastrophiques. C’est aussi un projet de recherche qui a démarré il y a vingt ans, et également un logiciel commercialisé par la société AbsInt, qui a été employé dans l’industrie pour compiler des logiciels embarqués critiques utilisés dans l’avionique et le nucléaire. Dans ces domaines, l’intérêt pour CompCert a résulté d’un besoin d’améliorer les performances du code produit, tout en garantissant des exigences de traçabilité requises par les processus de développement en vigueur dans ces domaines critiques, ce qu’a effectivement permis CompCert.

Le langage C a été conçu au début des années 70, afin de laisser davantage de liberté aux écrivains de compilateurs pour programmer au plus près de la machine. Ce langage n’a pas été conçu avec l’optique d’être mathématiquement défini. Établir la correction de CompCert a nécessité de définir une sémantique formelle du langage C qui décrit non seulement des programmes fournissant un résultat final (comme le compilateur jouet de 1972), mais aussi des programmes dont l’exécution ne termine jamais, comme ceux utilisés par les commandes de vol d’un avion. Le théorème de correction établit que ces comportements sont préservés lors de la compilation.

© Jean-Claude MOSCHETTI / IRISA / CNRS Images

Pour mener cette preuve, il a fallu résoudre plusieurs défis :

      1. se fonder sur des formalismes adaptés,
      2. avoir des principes de raisonnement associés (notamment proposer un style sémantique adapté au raisonnement inductif), et plus généralement une méthodologie de preuve passant à l’échelle, et enfin,
      3. disposer d’outils logiciels facilitant la mise en oeuvre de ces formalismes et automatisant le raisonnement.

CompCert a reçu plusieurs récompenses, dont l’ACM software system award en 2022, le prix le plus prestigieux décerné à un logiciel issu de la recherche, qui a par la passé été décerné aux compilateurs C les plus utilisés, GCC (2015) et LLVM (2012).

CompCert est un jalon. Il a montré qu’il est désormais possible de mener des preuves sur des objets aussi complexes que des compilateurs réalistes. Les formalismes et la méthodologie de preuve qu’il propose ont été réutilisés dans plusieurs projets de recherche en France et à l’étranger. Par exemple, à Rennes, nous poursuivons nos travaux dans le but de doter CompCert de davantage de possibilités de compilation, et d’offrir des garanties supplémentaires en matière de sécurité logicielle.

Sandrine Blazy

Pour aller plus loin retrouvez  :

      • La vidéo du CNRS à l’occasion de la Médaille d’argent de Sandrine
      • La vidéo pour le Prix ACM décerné au logiciel CompCert

Ce qu’il faut savoir sur les compilateurs et leur vérification (1/2)

Sandrine Blazy, Professeure à l’université de Rennes et directrice adjointe de l’IRISA, est une spécialiste des compilateurs et des logiciels sûrs. Elle a développé avec Xavier Leroy, CompCert, le premier compilateur pour le langage C vérifié à l’aide de Coq. Pour ce véritable tour de force scientifique et technique, elle a obtenu la médaille d’argent du CNRS (une des plus belles récompenses scientifiques en France). Si vous ne comprenez pas en quoi cela consiste, Sandrine va l’expliquer à binaire et ce sera l’occasion d’un peu mieux comprendre ce qui se passe dans un ordinateur. Serge Abiteboul et Pierre Paradinas
© Jean-Claude MOSCHETTI / IRISA / CNRS Images

Les débuts de l’informatique

Les liens entre mathématiques et informatique sont féconds. Dans les années quarante, la nécessité de mécaniser des calculs numériques permettant de résoudre des équations mathématiques a permis le développement des premières machines de calcul à grande échelle, qui ont préfiguré les premiers ordinateurs. Ces calculateurs universels enchaînaient en séquence des opérations mathématiques élémentaires, décomposant des calculs modélisant des phénomènes physiques. Aujourd’hui, ces calculs sont réalisés par une simple calculette de bureau.

Chaque opération était fidèlement décrite par un code constitué de commandes compréhensibles par la machine, c’est-à-dire des suites de chiffres zéros et un (signifiant l’absence et la présence de courant dans les composants d’un circuit électronique). Aussi, faire exécuter une opération par un calculateur était une véritable gageure. Les experts dont c’était le travail devaient encoder l’opération (c’est-à-dire trouver les nombres adéquats pour représenter l’opération, ainsi que les valeurs auxquelles elle s’appliquait qui étaient encodées sur des cartes perforées), en plus d’effectuer des manipulations physiques sur la machine. Ces experts écrivaient ces codes sur papier, avant de les fournir à la machine, dont ils devaient de plus comprendre le fonctionnement électromécanique. Ces premières machines étaient gigantesques et complexes à manipuler. En guise d’écran, des marteaux (tels que ceux utilisés par les machines à écrire) imprimaient sur papier des caractères. Par contre, elles avaient l’avantage de fonctionner sans cesse et d’accélérer grandement les temps de calcul de chaque opération, en enchaînant en des temps records des successions de calculs variés, ce qui a fait leur succès.

Le succès aidant et les calculs devenant de plus en plus complexes, il a été nécessaire de rendre l’écriture des codes moins absconse et d’automatiser davantage l’enchaînement des calculs. Une première réponse a été l’utilisation répandue d’une notation plus expressive et graphique (à l’aide de boîtes reliées par des flèches) pour représenter l’enchaînement des calculs. Les diagrammes résultants, appelés organigrammes permettaient de représenter simplement non seulement des séquences de calculs, mais aussi des décisions à prendre en fonction de résultats intermédiaires, et donc des enchaînements plus sophistiqués de calculs (comme la répétition d’étapes de calculs jusqu’à atteindre un certain seuil). Ces diagrammes permettaient de s’abstraire du matériel, et de décomposer un problème avant d’écrire du code. Plus faciles à comprendre par des humains, ils permettaient de réutiliser une opération lorsque la machine évoluait en fonction des progrès technologiques fréquents.

L’expressivité des organigrammes a favorisé l’émergence d’”algorithmes”, c’est-à-dire d’enchaînements plus efficaces des calculs (c’est-à-dire réduisant le temps de calcul), du fait de la représentation particulière des nombres en machine. Par exemple, en 1949, Alan Turing a proposé une nouvelle façon de calculer la fonction mathématique factorielle, sans utiliser les opérations coûteuses de multiplication mais seulement des additions. Il se demande alors comment être sûr que ce que calcule son organigramme est effectivement le même résultat que celui de la fonction factorielle du mathématicien, en d’autres termes que son organigramme est correct. Pour y répondre, il a effectué ce qu’on appellerait aujourd’hui la première preuve de programme, en annotant son organigramme avec des assertions, dont il a ensuite vérifié la cohérence.

L’effort pour démocratiser la mécanisation des calculs s’est poursuivi avec l’invention des premiers langages de programmation. Les organigrammes ont fait place au pseudo-code, puis aux algorithmes et programmes écrits dans un langage dont la syntaxe est plus intuitive. Un langage de programmation définit un ensemble de commandes abstraites mais précises pour effectuer toutes les opérations exprimables dans un organigramme, avec des mots-clés en anglais (plus faciles à appréhender que les seuls nombres d’un code). Le premier livre sur la programmation paraît en 1951, alors que très peu de machines sont en service; il est utilisé pour des recherches en physique, astronomie, météorologie et biochimie.

Les langages de programmations et les compilateurs

Le langage de programmation devient un intermédiaire nécessaire entre l’humain et la machine, et il devient indispensable d’automatiser la traduction des programmes en code machine. Le premier compilateur A-0 mis au point par Grace Hopper est disponible en 1952. Ce terme résulte de son premier usage, mettre bout à bout des portions de code, à la manière d’une bibliothécaire qui rassemble des documents sur un sujet précis. Pour expliquer de plus les possibilités prometteuses offertes par un tel programme de traduction (d’un langage source en un code machine), Grace Hopper utilise la métaphore d’une ligne de production dans une usine, qui produirait des nombres (plutôt que des automobiles) et plus généralement des données au moyen d’outils (tables de calcul, formules, calculs numériques).

Le compilateur devient un point de passage obligé pour traduire tout programme écrit par un humain en un code compréhensible par la machine, et la traduction de l’un vers l’autre est un défi scientifique. En effet, un problème se pose du fait de la faible vitesse des calculs, des capacités très limitées de stockage, mais aussi de l’abstraction et la généralité des programmes écrits : plus le programme source est facile à comprendre pour un humain, moins l’exécution du code machine engendré est efficace.

File:Fortran logo.svgEn 1953, le langage Fortran est le premier à être dédié au calcul numérique, et donc à s’abstraire du matériel spécifique à une machine. C’est aussi le premier qui devient un standard: pour la première fois, les programmeurs parlent un même langage, quelle que soit la machine qu’ils utilisent. IBM consacre un effort notable à développer son compilateur, afin qu’il produise un code efficace. C’est le début de l’invention de nouvelles techniques de compilation, les premières optimisations (ex. compiler séparément des portions de code, ou encore détecter des calculs communs pour les factoriser). Le manuel de Fortran est disponible en 1956, et son compilateur en 1957.

Cet effort pour démocratiser la programmation se poursuit avec le langage Cobol dédié au traitement des données. Désormais, l’ordinateur ne calcule pas que des nombres; il permet plus généralement de structurer des données et de les traiter efficacement. COBOL ouvre la voie à de nouvelles applications. Le premier programme COBOL est compilé en 1960; en 1999 la grande majorité des logiciels seront écrits en COBOL, suite à son utilisation massive dans les domaines de la banque et de l’assurance. Ainsi, dans les années 60, la pratique de la programmation se répand et devient une science; les langages de programmation foisonnent. Aujourd’hui encore, les langages de programmation évoluent sans cesse, pour s’adapter aux nouveaux besoins.

Sandrine Blazy

Pour aller plus loin retrouvez  :

      • La vidéo du CNRS à l’occasion de la Médaille d’argent de Sandrine
      • La vidéo pour le Prix ACM décerné au logiciel CompCert

Les Metavers peuvent-il se mettre au vert ?

Loin d’être immatériel, le numérique est par nature ambivalent vis à vis des enjeux environnementaux. Il incarne d’un côté la promesse de catalyser des solutions pour réduire les pollutions d’autres secteurs (agriculture, énergie, mobilité, bâtiment, etc.), mais d’un autre côté il est également lui même source d’externalités négatives directes et indirectes. Benjamin Ninassi et Marie Véronique Gauduchon nous détaillent cette dualité. Pascal Guitton, Serge Abiteboul.

Réalisée avec Midjourney

Le secrétaire général adjoint de l’Union Internationale des Télécommunications l’a rappelé en septembre 2023  : pour tenir l’Accord de Paris sur le climat, le numérique doit réduire de 45% ses émissions de Gaz à Effet de Serre d’ici 2030, et les diviser par 10 d’ici 2050, conformément à la trajectoire Science Based Target Initiative (SBTi). Il a également rappelé que cette réduction doit se faire tout en permettant l’émergence et le déploiement de solutions en faveur de la décarbonation d’autres secteurs.

Or la tendance actuelle en France, d’après l’étude ADEME/ARCEP de début 2023, est à une augmentation de 45% des émissions liées à nos usages numériques d’ici 2030.

Des scénarios incompatibles

Cette incompatibilité entre la trajectoire cible et de la tendance actuelle en matière de lutte contre le réchauffement climatique apparaît comme un enjeu majeur de la transition environnementale du secteur. A noter qu’en plus de participer à l’émission de GES, le numérique contribue à dépasser d’autres limites planétaires, à travers par exemple l’activité extractive nécessaire à la production des métaux qui composent les équipements. D’ailleurs, indépendamment des enjeux environnementaux, se pose une question de disponibilité de certaines ressources métalliques critiques dont la plupart sont en concurrence avec d’autres transitions comme la production d’énergie décarbonée ou l’électrification de la mobilité.

Derrière la notion de Métavers, il y a surtout une agrégation de technologies qui sert une finalité, un usage. La question pour demain n’est pas tant de savoir s’il faut aller ou pas vers le Métavers, mais de définir quels usages du numérique sont compatibles avec la trajectoire environnementale cible, quels usages peuvent réellement contribuer à réduire les impacts environnementaux d’autres secteurs, en se substituant par exemple à des usages plus carbonés. Cette évaluation des gains doit se faire dans un cadre méthodologique standardisé, systémique, intégrant les effets rebonds et allant au delà des effets d’annonce.

Une nécessaire planification de la décroissance des impacts

Pour tenir un budget, afin d’éviter les crises, il est nécessaire de planifier en amont ses dépenses. Cette planification se fait en deux phases : une phase de priorisation pour hiérarchiser les dépenses selon leur importance, et une phase de quantification afin de ne pas finir en négatif.  Ainsi, le budget devient le cadre d’opération. Comme dit plus haut, le cadre environnemental pour le secteur du numérique, c’est une réduction de -45% de ses émissions de GES d’ici 2030, et une division par 10 d’ici 2050.

Heureusement, plusieurs leviers sont activables pour réduire les impacts du numérique, à commencer par poursuivre et accélérer les travaux de recherche et leur déploiement dans l’industrie sur la frugalité des algorithmes, l’écoconception logicielle, l’amélioration du refroidissement et la réduction de la consommation énergétique des centres de données. Mais malgré ces travaux en cours depuis de nombreuses années maintenant, la tendance actuelle le prouve : optimiser une partie du système ne suffit pas dans un contexte de croissance des usages et du nombre d’utilisateurs au niveau mondial. Pour limiter les effets rebonds, il apparaît nécessaire de combiner ces gains d’efficacité à une indispensable sobriété numérique, en agissant aussi sur les usages.

Le Secrétariat Général à la Planification Écologique a d’ailleurs courageusement entamé cet exercice. Dans un rapport sur la planification écologique dans l’énergie on peut y voir une proposition de hiérarchisation des usages de la biomasse locale avec une liste d’usages considérés comme prioritaires, d’usages à interroger (parmi lesquels figure par exemple le trafic aérien), et enfin une liste d’usages à réduire.

Le numérique a besoin de la même démarche, afin de pouvoir planifier et organiser sa décarbonation, en hiérarchisant ses usages.

Comme pour les autres secteurs, il ne s’agit pas de faire ces choix à un niveau technologique, et d’opposer l’Intelligence Artificielle à l’Internet des Objets ou aux technologies immersives : c’est au niveau des usages, des fournisseurs de services numériques et de plateformes que les enjeux de régulation se situent et que cette priorisation doit intervenir.

Ne plus confondre la fin et les moyens : revenir à l’usage, au service rendu

Cette nécessité se retrouve d’ailleurs dans le Référentiel Général de l’Écoconception des Services Numériques, ouvert jusque fin novembre 2023 à la consultation publique, et qui pourrait être un levier activable d’une stratégie de décarbonation du secteur. Son premier critère est rédigé ainsi : « Le service numérique a-t-il été évalué favorablement en termes d’utilité en tenant compte de ses impacts environnementaux ? »

Une fois qu’on aura priorisé ces usages et permis de questionner l’utilité, il apparaît nécessaire d’être en mesure d’évaluer les impacts, toujours dans cette logique budgétaire. Concernant les Métavers et le secteur de la culture numérique, des travaux sont en cours, d’ailleurs en partie financés par le ministère de la Culture. Parmi ces initiatives on retrouve par exemple le calculateur carbone Jyros pour le secteur des jeux vidéo, ou le projet CEPIR qui produit les premières données d’impacts environnementaux d’œuvres immersives. Améliorer la fiabilité de ces évaluations nécessite de poursuivre et même d’accélérer ces travaux dans une optique de standardisation méthodologique.

Aucun scénario prospectif compatible avec l’Accord de Paris n’envisage à ce stade un déploiement massif dans tous les foyers de nouveaux équipements connectés qui s’additionneraient à l’existant, comme les smartphones se sont ajoutés aux télévisions, aux ordinateurs, aux tablettes, et dont les cycles d’évolution technologique sont très courts, ce qui est le cas des casques de réalité virtuelle. Un numérique résilient et durable est un numérique qui stabilise et réduit le renouvellement des équipements, qui permet la substitution et non l’empilement. Le secteur du numérique, comme les autres secteurs, a besoin de faire preuve de techno-discernement. Cette approche consiste à imaginer, construire, déployer les services, outils et plateformes numériques de demain, qui fonctionnent au maximum avec les infrastructures et les équipements d’aujourd’hui voire d’hier. Cette approche, qui peut s’apparenter à une approche low-tech pour le numérique, est à développer aussi bien via des travaux de recherche multidisciplinaires que via l’émergence de solutions industrielles innovantes. Elle nécessite de s’intéresser tout autant aux usages qu’aux technologies et aux infrastructures sur lesquelles elles s’appuient.

Mais d’ailleurs, peut-il exister des Métavers low-tech ?

Réalisée avec Midjourney

Malgré ces constats, certains usages des technologies immersives pourraient être compatibles avec la trajectoire SBTi, par exemple en réduisant l’impact de la mobilité en se substituant à des déplacements nécessairement carbonés.

Un exemple qui va dans le sens du low-tech, c’est de miser sur des technologies déjà massivement déployées, à l’image de workadventure . Cette solution open source permet de contrôler un avatar dans un environnement virtuel en 2D à travers un simple navigateur web, et d’interagir via les périphériques (caméra, micro, etc.) du terminal avec les autres avatars à proximité. Le renforcement de la co-présence et de l’immersion par rapport à la visioconférence classique, sans introduire de nouveaux équipements, est un enjeu environnemental important pour réduire l’impact de la mobilité professionnelle.

Mutualiser et partager, justice climatique et justice numérique

Une autre forme de Métavers à faible impact serait basée sur la mutualisation d’équipements immersifs via les centres culturels comme des médiathèques par exemple, à l’image d’une des propositions du rapport exploratoire sur le Métavers, permettant la visite de sites culturels inaccessibles via une mobilité bas carbone. Un avantage majeur de mutualiser l’accès est de rendre caduque la captation de données personnelles, et le développement d’une économie de l’attention basée sur le traitement et la collecte de ces données. En effet, la collecte, le stockage et le traitement de données personnelles et d’usage des plateformes nécessitent d’importantes quantités de ressources matérielles et d’énergie. Ces dépenses servent directement certains modèles économiques (économie de l’attention, ciblage publicitaire) et non pas le service final rendu aux usagers.

En augmentant exponentiellement les possibilités d’interaction, les Métavers permettraient de capter des quantités d’autant plus astronomiques de données.

Il y a donc un enjeu environnemental important à réguler les usages pour ne pas permettre à ce type de modèle économique d’être transposé dans de futurs mondes immersifs.

Réalisée avec Midjourney

Enfin, à une échelle mondiale une question d’équité majeure se pose. Dans le cadre d’un budget environnemental compatible avec l’Accord de Paris, il est donc nécessaire d’opérer des arbitrages. Peut-on raisonnablement à la fois envisager envoyer dans des Métavers high-tech une population déjà par ailleurs largement connectée et outillée numériquement, tout en ayant les ressources nécessaires pour déployer les infrastructures réseaux, les centres de données et les deux ou trois milliards de terminaux permettant de connecter à internet les 33% de la population mondiale qui ne l’est toujours pas en 2023 ?

Benjamin Ninassi, Adjoint au responsable du programme Numérique et Environnement d’Inria
& Marie Véronique Gauduchon, Conseillère impact environnemental VR – CEPIR (Cas d’études pour un immersif responsable).