Discussion :

[Bill Fassinou]

Rust 1.51 est disponible avec Resolver, une nouvelle fonctionnalité pour Cargo
et l'implémentation MVP des const generics

Rust est un langage de programmation développé par Mozilla Research. Il est open source et son code est disponible sur GitHub. Ses domaines de prédilection sont la programmation système, les applications en ligne de commande, les applications Web via WebAssembly, les services réseau et les systèmes embarqués. Rust a été conçu pour faciliter le développement rapide et sûr de logiciels au niveau système. Selon ses auteurs, l'approche unique de Rust permet d'obtenir un meilleur code avec moins de compromis que C, C++, Go et les autres langages que vous utilisez probablement.

Rust est mis à jour régulièrement, souvent tous les mois. Ainsi, si vous avez déjà installé une version antérieure de Rust via rustup, vous pouvez accéder à la dernière version en tapant la commande suivante :

Code :

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

$ rustup update stable

Publiée le 25 mars 2021, la version Rust 1.51.0 est définie par l'équipe comme l'un des plus grands ajouts au langage et au gestionnaire de paquets Cargo depuis un certain temps. Dans cette version, il y a notamment la stabilisation d'une implémentation MVP (minimum viable product) des const generics et un nouveau "résolveur de fonctionnalités" pour Cargo. Voici un aperçu des changements intervenus dans cette version.

Implémentation MVP des const generics

Avec l'implémentation MVP des const generics, un outil est ajouté pour les concepteurs de bibliothèques afin de développer des API sûres au moment de la compilation. Fonction très attendue, les const generics sont des arguments génériques qui portent sur des valeurs constantes, plutôt que sur des types ou des durées de vie. Cela permet aux types d'être paramétrés par des entiers, par exemple. L'équipe prévoit d'introduire progressivement les const generics, de sorte que les seuls types qui peuvent être utilisés comme type d'un argument const generic sont actuellement les types d'entiers, y compris size, usize, char et bool.

En effet, avant cette version, Rust vous permettait de paramétrer vos types sur des durées de vie ou des types. Par exemple, si vous vouliez avoir une structure qui soit générique sur le type d'élément d'un tableau, vous écririez ce qui suit :

Code Rust :

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

1
2
3
4
5
struct FixedArray<T> {
              // ^^^ Type generic definition
    list: [T; 32]
        // ^ Where we're using it.
}

Si vous utilisez ensuite FixedArray<u8>, le compilateur créera une version monomorphe de FixedArray qui ressemblera à ceci :

Code Rust :

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

1
2
3
struct FixedArray<u8> {
    list: [u8; 32]
}

Selon l'équipe de Rust, il s'agit d'une fonctionnalité puissante qui vous permet d'écrire du code réutilisable sans frais d'exécution. Cependant, jusqu'à cette version, il n'était pas possible d'être facilement générique sur les valeurs de ces types. Cela était particulièrement vrai pour les tableaux qui incluent leur longueur dans leur définition de type ([T ; N]), sur lesquels il était auparavant impossible d'être générique. Maintenant, avec la version 1.51.0, vous pouvez écrire du code qui est générique sur les valeurs de n'importe quel type integer, bool, ou char (l'utilisation de valeurs struct ou enum est toujours instable).

Ce changement vous permet maintenant d'avoir votre propre structure de tableau qui est générique sur son type et sa longueur. Examinons un exemple de définition et la façon dont elle peut être utilisée.

Code Rust :

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

1
2
3
4
5
struct Array<T, const LENGTH: usize> {
    //          ^^^^^^^^^^^^^^^^^^^ Const generic definition.
    list: [T; LENGTH]
    //        ^^^^^^ We use it here.
}

Maintenant si vous utilisez Array<u8, 32>, le compilateur fera une version monomorphe de Array qui ressemble à :

Code Rust :

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

1
2
3
struct Array<u8, 32> {
    list: [u8; 32]
}

Stabilisation de array::IntoIter

Avec les const generics, une nouvelle API a été stabilisée qui les utilise, std::array::IntoIter. Intolter permet aux développeurs de créer un itérateur par valeur sur n'importe quel tableau. Auparavant, il n'y avait pas de moyen pratique d'itérer sur les valeurs possédées d'un tableau, seulement sur les références à celles-ci.

Code Rust :

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

1
2
3
4
5
6
7
8
9
10
11
12
13
fn main() {
  let array = [1, 2, 3, 4, 5];
 
  // Previously
  for item in array.iter().copied() {
      println!("{}", item);
  }
 
  // Now
  for item in std::array::IntoIter::new(array) {
      println!("{}", item);
  }
}

Notez que ceci est ajouté en tant que méthode séparée au lieu de .into_iter() sur les tableaux, car cela introduit actuellement un certain nombre de ruptures. Pour le moment, .into_iter() fait référence à l'itérateur de tranche par référence. L'équipe explore les moyens de rendre cela plus ergonomique à l'avenir.

Resolver : nouvelle fonctionnalité de Cargo

D'après l'équipe, la gestion des dépendances est un problème difficile, et l'une des parties les plus difficiles est de choisir la version d'une dépendance à utiliser lorsqu'elle est dépendante de deux paquets différents. Cela ne comprend pas seulement son numéro de version, mais aussi les fonctionnalités qui sont ou ne sont pas activées pour le paquet. Le comportement par défaut de Cargo consiste à fusionner les fonctionnalités d'un seul paquet lorsqu'il est mentionné plusieurs fois dans le graphe des dépendances.

Par exemple, lorsque que vous avez une dépendance appelée foo avec les fonctionnalités A et B, qui est utilisée par les paquets bar et baz, mais bar dépend de foo+A et baz dépend de foo+B. Cargo fusionnera ces deux fonctionnalités et compilera foo comme foo+AB. L'avantage est que vous n'avez à compiler foo qu'une seule fois, et qu'il peut ensuite être réutilisé pour bar et baz. Cependant, cela comporte aussi un inconvénient. Que faire si une fonctionnalité activée dans une dépendance de construction n'est pas compatible avec la cible pour laquelle vous construisez ?

Un exemple commun de ceci dans l'écosystème est la fonctionnalité optionnelle std incluse dans beaucoup de crates #![no_std], qui permet aux crates de fournir des fonctionnalités supplémentaires lorsque std est disponible. Imaginez maintenant que vous voulez utiliser la version #![no_std] de foo dans votre binaire #![no_std], et utiliser foo au moment de la construction dans votre build.rs. Si votre dépendance au moment de la construction dépend de foo+std, votre binaire dépend maintenant aussi de foo+std, ce qui signifie qu'il ne compilera plus, car std n'est pas disponible pour votre plateforme cible.

C'est un problème de longue date dans Cargo, et avec cette version il y a une nouvelle option resolver dans votre Cargo.toml, où vous pouvez définir resolver="2" pour dire à Cargo d'essayer une nouvelle approche pour résoudre les fonctionnalités. Vous pouvez consulter la RFC 2957 pour une description détaillée du comportement, qui peut être résumée comme suit.

• dépendances de développement : lorsqu'un paquet est partagé en tant que dépendance normale et dépendance de développement, les fonctionnalités de la dépendance de développement ne sont activées que si la construction actuelle inclut des dépendances de développement ;
• dépendances hôte : lorsqu'un paquet est partagé en tant que dépendance normale et en tant que dépendance de construction ou proc-macro, les fonctionnalités de la dépendance normale sont conservées indépendamment de la dépendance de construction ou proc-macro ;
• dépendances de cible : lorsqu'un paquet apparaît plusieurs fois dans le graphe de construction, et que l'une de ces instances est une dépendance spécifique à la cible, les fonctionnalités de la dépendance spécifique à la cible ne sont activées que si la cible est en cours de construction.

Par ailleurs, l'équipe informe que, bien que cela puisse entraîner la compilation de certains crates plus d'une fois, cela devrait fournir une expérience de développement beaucoup plus intuitive lors de l'utilisation de fonctionnalités avec Cargo. Si vous souhaitez en savoir plus, vous pouvez également lire la section "Feature Resolver" dans le Cargo Book pour plus d'informations.

Code :

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

1
2
3
4
5
[package]
resolver = "2"
# Or if you're using a workspace
[workspace]
resolver = "2"

Fractionnement des informations de débogage

Selon l'équipe, cette version marque l'une des plus grandes améliorations depuis longtemps pour Rust sur macOS. Les informations de débogage font correspondre le code binaire à votre code source, afin que le programme puisse vous donner plus d'informations sur ce qui s'est mal passé lors de l'exécution. Sous macOS, les informations de débogage étaient auparavant rassemblées dans un seul dossier .dSYM à l'aide d'un outil appelé dsymutil, ce qui peut prendre un certain temps et occuper pas mal d'espace disque.

La collecte de toutes les informations de débogage dans ce répertoire permet de les retrouver au moment de l'exécution, en particulier si le binaire est déplacé. Cependant, il y a un inconvénient : même si vous apportez une petite modification à votre programme, dsymutil devra parcourir tout le binaire final pour produire le dossier .dSYM final. Cela peut parfois ajouter beaucoup au temps de construction, surtout pour les grands projets, car toutes les dépendances sont toujours récupérées, mais c'est une étape nécessaire, car sans elle, la bibliothèque standard de Rust ne savait pas comment charger les informations de débogage sur macOS.

Récemment, les backtraces Rust sont passés à l'utilisation d'un backend différent qui supporte le chargement des informations de débogage sans avoir besoin d'exécuter dsymutil, et l'équipe a stabilisé le support pour sauter l'exécution de dsymutil. Selon elle, cela peut accélérer de manière significative les constructions qui incluent des debuginfo et réduire de manière significative l'espace disque utilisé.

API stabilisées

Au total, cette version a vu la stabilisation de 18 nouvelles méthodes pour divers types comme slice et Peekable. Un ajout notable est la stabilisation de ptr::addr_of! et ptr::addr_of_mut!, qui vous permettent de créer des pointeurs bruts vers des champs non alignés. Auparavant, cela n'était pas possible parce que Rust exige que &/&mut soit aligné et pointe vers des données initialisées, et que &addr en tant que *const _ provoquerait alors un comportement non défini puisque &addr doit être aligné. Ces deux macros vous permettent maintenant de créer en toute sécurité des pointeurs non alignés. Les méthodes suivantes ont été stabilisées.

• Arc::decrement_strong_count ;
• Arc::increment_strong_count ;
• Once::call_once_force ;
• Peekable::next_if_eq ;
• Peekable::next_if ;
• Seek::stream_position ;
• array::IntoIter ;
• panic::panic_any ;
• ptr::addr_of! ;
• ptr::addr_of_mut! ;
• slice::fill_with ;
• slice::split_inclusive_mut ;
• slice::split_inclusive ;
• slice::strip_prefix ;
• slice::strip_suffix ;
• str::split_inclusive ;
• sync::OnceState ;
• task::Wake.

Source : Rust 1.51.0

Et vous ?

Que pensez-vous des nouveautés de Rust 1.51 ?

Voir aussi

Rust 1.50.0 est disponible et s'accompagne de l'indexation de tableau générique Const, ainsi que des affectations sécurisées aux champs d'union ManuallyDrop<T>

Évolution de l'écosystème Rust en 2020 : Rust continue de faire des percées en tant que langage utilisé pour la production, les développeurs réclament une plus grande interopérabilité avec C++

Microsoft, Google, AWS, Huawei et Mozilla s'associent pour créer la Fondation Rust, une organisation à but non lucratif chargée de gérer le langage de programmation

Rust 1.49.0 est disponible avec l'amélioration des supports de Linux ARM 64 bits, macOS et Windows ARM 64 bits

[Invité]

Ma hiérarchie aimerait utiliser Rust. J'ai fait part de mes réserves quant aux lois américaines sur les restrictions à l'export. C'est d'autant plus vrai maintenant que le développement du langage est chapeauté par une fondation basée aux USA.

Le fait d'avoir des parties de code en Rust, et comme il n'existe qu'un seul compilateur, pourrait nous empêcher de vendre nos solutions dans des pays en froid avec les USA.

[Uther]

Que pensez-vous des nouveautés de Rust 1.51 ?

Les const generics, sont vraiment une grosse amélioration du langage que j'attendais depuis un moment. S'ils pouvaient évoluer assez pour devenir de vrais type dépendants, ça serait vraiment énorme.

Ma hiérarchie aimerait utiliser Rust. J'ai fait part de mes réserves quant aux lois américaines sur les restrictions à l'export. C'est d'autant plus vrai maintenant que le développement du langage est chapeauté par une fondation basée aux USA.

Le fait d'avoir des parties de code en Rust, et comme il n'existe qu'un seul compilateur, pourrait nous empêcher de vendre nos solutions dans des pays en froid avec les USA.

Au contraire Rust dépend moins des USA que la plupart des langages de programmation, étant donné que la fondation Rust n'est pas propriétaire du langage Rust. C'est juste une institution qui gère l'utilisation des contributions financières au langage. Les différentes équipes qui supervisent l'évolution du langage sont internationales et ne sont rattachées à aucune entité légale. La propriété de Rust est uniquement attribuée à ses contributeurs.

Copyrights in the Rust project are retained by their contributors. No copyright assignment is required to contribute to the Rust project.

Après, si les USA veulent te faire chier, il le feront, quelque soit les logiciels que tu utilises, mais il n'y a aucune raison que ça pose plus de problèmes pour le Rust que pour la plupart des langages, y compris le C et le C++ pour lesquels tous les principaux fournisseurs de compilateurs ainsi que toutes les fondations supervisant les principaux compilateurs libres sont aussi domiciliés aux USA. D'ailleurs, à ma connaissance, GCC n'a jamais eu ce genre de soucis alors que la FSF, propriétaire du projet est domiciliée aux USA.

[denisys]

Ma hiérarchie aimerait utiliser Rust. J'ai fait part de mes réserves quant aux lois américaines sur les restrictions à l'export. C'est d'autant plus vrai maintenant que le développement du langage est chapeauté par une fondation basée aux USA.

Le fait d'avoir des parties de code en Rust, et comme il n'existe qu'un seul compilateur, pourrait nous empêcher de vendre nos solutions dans des pays en froid avec les USA.

J’ai pas bien compris ton point de vue !
Que veut tu dire par : les lois américaines sur les restrictions à l'export.
Tu veux exporter le langage Rust ?
Ou.
Exporter une application développée en langage Rust ?

[Invité]

J’ai pas bien compris ton point de vue !
Que veut tu dire par : les lois américaines sur les restrictions à l'export.
Tu veux exporter le langage Rust ?
Ou.
Exporter une application développée en langage Rust ?

Je veux pouvoir exporter un programme et toutes ses dépendances en format binaire sans tomber sous le joug des lois américaines.

À partir où les dites dépendances sont développées par des Américains, où le code ou les binaires sont hébergés sur des serveurs américains, ou un langage tout entier est chapeauté par une fondation américaine, c'est le flou artistique au niveau des restrictions à l'export.

Et adopter une techno comme Rust est un choix stratégique à long terme. C'est pas le genre de langage qu'on utilise 6 mois pour ensuite passer à autre chose.

[denisys]

Je veux pouvoir exporter un programme et toutes ses dépendances en format binaire sans tomber sous le joug des lois américaines.

À partir où les dites dépendances sont développées par des Américains, où le code ou les binaires sont hébergés sur des serveurs américains, ou un langage tout entier est chapeauté par une fondation américaine, c'est le flou artistique au niveau des restrictions à l'export.

Et adopter une techno comme Rust est un choix stratégique à long terme. C'est pas le genre de langage qu'on utilise 6 mois pour ensuite passer à autre chose.

OK !!
Je voie mieux le problème que tu aborde.
Sauf,que dans ce que je comprends, dans l’expression de ton point de vue.
Tu prends le diapason à l’envers.
Pour comprendre, où est le début du Spaghetti.
Sans, appréhender, ce que peut être la fin du Spaghetti.
Dans ton appréhension, bien que tu n’a pas fondamentalement faux.
Il faut bien distinguer, le périmètre législatif, propriétaire et commercial, de toute production.
Que ce soit une production logiciel, mécanique, de produit semi fini ou fini.
Pour bien comprendre, la partie, qui te fait douter, d’un choix, comparé à un autre.
Je vais, sans, faire de pub pour cette société, malgré tous prendre exemple, de cette société.
Pour bien te faire comprendre, les périmètres législatifs, en fonction des législations de sa nation.

Si toi et moi, prenons en exemple les restrictions de distribution, des produits logiciels, de la société ORACLE.
Car, je pense, que c’est ici, que tu prends source, des restrictions, de diffusions et de revente.

ORACLE, est une société US, dont le siège social est basé aux USA.
ORACLE, est dans l’obligation, de respecter, la législation de son pays.
Lorsque, ORACLE, applique la politique de restriction de commercialisation et diffusion de ces produits.
Cela s’applique, pour toutes ces antennes, à travers le monde.
Même, pour ORACLE France. ORACLE France. , ne peut commercialiser un produit, dans un pays, étant sous restriction par le gouvernement US.

Mais, il y a une segmentation, qu’il faut bien comprendre.
Cette segmentation, ce divise sur 2 point.
Le produit logiciel, est développé, avec un langage de programmation :
Propriétaire.
Ou
Commun.

Dans les langages de programmation, propriétaire.
Quelque exemple me vienne à l’esprit.
ABAP de SAP.
Formula d’IBM.

Dans les langages communs.
Et bien effectivement, tu a les standards ; C, CPP, Turbo Pascal, etc...
Sans compter les langages de scripts : Perl, Python, etc...

Rust, n’étant pas un langage propriétaire.
Celui-ci n’est pas soumit a restriction, d’utilisation.

Est-ce que Java, c ou c++, sont soumit a restriction d’utilisation ???
Si, oui, par quel pays ???

Si comme, ces langages de programmation, Rust, n’est pas soumis à des restrictions.
Seul, le produit logiciel peut l’être.
Et, si tu est en France.
N’oublie, que la nation, dans lequel tu est, peut restreindre, toutes commercialisations, avec des pays tiers, considères, comme étant, dangereux, envers la nation France.
Mais, l’UE, peut également, emmètre des restrictions, non considérés, par la nation France.

[ormond94470]

Ma hiérarchie aimerait utiliser Rust. J'ai fait part de mes réserves quant aux lois américaines sur les restrictions à l'export. C'est d'autant plus vrai maintenant que le développement du langage est chapeauté par une fondation basée aux USA.

Le fait d'avoir des parties de code en Rust, et comme il n'existe qu'un seul compilateur, pourrait nous empêcher de vendre nos solutions dans des pays en froid avec les USA.

Je n'ose imaginer le temps et l'argent que tu fais perdre à ta boîte à cause de raisonnement plus que douteux... Ça ne serait pas plutôt que tu ne maîtrises pas ce langage et que tu as peur d'être dépassé \ remplacé ?

[Uther]

Je veux pouvoir exporter un programme et toutes ses dépendances en format binaire sans tomber sous le joug des lois américaines.

À partir où les dites dépendances sont développées par des Américains, où le code ou les binaires sont hébergés sur des serveurs américains, ou un langage tout entier est chapeauté par une fondation américaine, c'est le flou artistique au niveau des restrictions à l'export.

Mais qu'est ce que tu proposes à ton entreprise, à la place de Rust, comme langage sans la moindre dépendance à du code produit par des américains ?

Parce j'ai beau chercher, je ne trouve aucun compilateur généraliste qui convienne à tes critères. Tous les principaux compilateurs C, C++, Python, Go, Ada, JavaScript, Pascal, D, PHP, ... ainsi que tous ceux basé sur la JVM (Java, Scala, Kotlin...) ou .net (C#, F#,...) sont propriété ou dépendent lourdement de code qui appartient à des sociétés ou à des fondations basées aux USA.

En fait Rust est certainement un des langage le moins lié légalement aux États-Unis, vu qu'il appartient à ses contributeurs et que les groupes de travail qui chapeautent son évolution sont internationaux et indépendant de toute institution. Alors certes on peut dire qu'il appartient partiellement aux USA vu que certains de ses milliers de contributeurs sont Américains, mais c'est déjà mieux que la plupart des langages, vu qu'ils appartiennent totalement à des sociétés ou des fondation américaines.
La fondation Rust est juste une association en support qui ne possède aucun droit de décision sur le langage.

Parmi toutes les raisons de ne pas utiliser Rust, le risque de restriction à l'export est certainement une des plus mauvaises.

[Invité]

il c'est déjà mieux que quasiment tous les langages, vu qu'ils appartiennent totalement à des sociétés ou des fondation américaines.

Pourquoi ? En quoi C ou C++, par exemple, "appartiennent" plus aux américains que Rust ?

Et sinon je crois que Caml vient de la recherche française, mais pas sûr que ce soit une meilleure solution...

[Uther]

Pourquoi ? En quoi C ou C++, par exemple, "appartiennent" plus aux américains que Rust ?

Et sinon je crois que Caml vient de la recherche française, mais pas sûr que ce soit une meilleure solution...

Le langage C en lui même n'appartient en effet pas aux USA. Mais comme le souci de Jeff_67 c'est les dépendances, le problème c'est les compilateurs pour le langage. Or GCC appartient à la Free Software Fondation, Visual C++ appartient a Microsoft, C++ Builder a Embarcadero, et inutile de préciser a qui appartient le Intel C++ compiler. Tout ceci correspond a des sociétés ou Fondations basées aux USA.

La seule exception parmi les gros est Clang qui a une politique de copyright similaire à Rust.

[Invité]

Le langage C en lui même n'appartient en effet pas aux USA. Mais comme son souci c'est les dépendances, le problème c'est les compilateurs pour le langage. Or GCC appartient à la Free Software Fondation, Visual C++ appartient a Microsoft, C++ Builder a Embarcadero, et inutile de préciser a qui appartient le Intel C++ compiler. Tout ceci correspond a des sociétés ou Fondations basées aux USA.

La seule exception parmi les gros est Clang qui a une politique de copyright similaire à Rust.

Voila, donc niveau license clang/llvm est similaire à Rust. Il y a aussi CompCert, qui a une double license et dépend d'une entreprise allemande. Et certainement d'autres.

[Uther]

En tout cas pour tous les compilateurs connus, c'est au mieux similaire au Rust, donc sauf s'il utilisaient déjà un compilateur de niche du type de CompCert, l’argument de base me parait très difficilement recevable.

[Invité]

En tout cas pour tous les compilateurs connus, c'est au mieux similaire au Rust, donc sauf s'il utilisaient déjà un compilateur de niche du type de CompCert, l’argument de base me parait très difficilement recevable.

Donc le C a une norme, différentes implémentations de compilateurs et même un compilateur vérifié formellement, mais ce n'est pas recevable. Rust n'a pas de norme et n'a qu'un compilateur mais c'est au moins aussi bien...

[Uther]

Je n'ai pas dit que le C n'avait pas certains points dignes d’intérêt (un compilateur certifié en est un), mais à moins qu'il utilise actuellement un des compilateurs de niche qui sont entièrement développés par des sociétés non américaines, l'argument règlementaire n'est pas recevable.

Un compilateur certifié, c'est très bien car ça apporte une garantie contre les erreur d'implémentation de la norme. Mais il faut quand même garder a l'esprit que la norme du C est bourrée de cas indéfinis ou le compilateur peut faire absolument n'importe quoi sans enfreindre la norme. Un des intérêts de Rust est justement de ne pas avoir ces cas indéfinis, qui sont des problèmes plus fréquent que les erreurs d'implémentation du compilateur. Si le programme que l'on développe avec un compilateur C certifié, n'est pas lui-même certifié, il est probablement plus sûr d'utiliser Rust.

L'idéal serait d'avoir à la fois un langage avec une norme stricte et un compilateur certifié, mais forcément c'est plus complexe. Il y a des efforts en cours pour certifier au moins partiellement Rust mais il y en a probablement encore pour quelque années (pour le moment seul le système de typage de Rust a été certifié).

[Invité]

Un compilateur certifié, c'est très bien car ça apporte une garantie contre les erreur d'implémentation de la norme. Mais il faut quand même garder a l'esprit que la norme du C est bourrée de cas indéfinis ou le compilateur peut faire absolument n'importe quoi sans enfreindre la norme. Un des intérêts de Rust est justement de ne pas avoir ces cas indéfinis, qui sont des problèmes plus fréquent que les erreurs d'implémentation du compilateur. Si le programme que l'on développe avec un compilateur C certifié, n'est pas lui-même certifié, il est probablement plus sûr d'utiliser Rust.

Sauf que... non :
"Ce projet développe essentiellement un compilateur, CompCert C, pour le langage C (ISO C90 / ANSI C avec quelques limitations mineures et plusieurs extensions inspirées des normes ultérieures) entièrement écrit et prouvé avec le logiciel Coq. [...] Ce compilateur possède une preuve vérifiée par machine que le code généré se comporte de la même manière que le code source." https://fr.wikipedia.org/wiki/CompCert

[Uther]

J'ai vraiment l'impression que tu ne lis pas ce que j'écris. Ton extrait ne fait que confirmer mon propos : l'intérêt d'un compilateur certifié, c'est qu'il est prouvé que le code source est compilé comformément a la norme, ce qui est une bonne chose.

Mais comme la norme contient de nombreux cas explicitement non définis, ça n'empêche pas qu'il faut s'assurer que ton programme ne les déclenche pas.

Une des intérêts de Rust, même s'il n'est pas formellement prouvé qu'il fait parfaitement son travail, c'est qu'il ne laisse pas de comportement non défini (en dehors des bloc unsafe)

[Invité]

Mais comme la norme contient de nombreux cas explicitement non définis, ça n'empêche pas qu'il faut s'assurer que ton programme ne les déclenche pas.

Oui, je crois que les chercheurs qui ont travaillé sur le projet pendant plusieurs années ont pensé à cela et en parlent dans leur doc et dans leurs articles.
Et ça ne change rien au fait que le C a des compilateurs indépendants des USA et/ou vérifiés formellement.