Merci ! Ça répond exactement à ma question. J'aurais du regarder directement là
Ma réponse du dessous tombe à l'eau, maintenant. :-P
Cependant on peut quand même se poser quelques questions parce que ce n'est pas vraiment rassurant de lire ensuite :
So, I conjecture that OCaml will not miscompile any Malfunction program, or at least that when it does, it will also miscompile a sufficiently contrived OCaml program.
Cela montre surtout qu'il reste encore du travail à faire dessus, mais tout comme lui, sa conjecture me semble plus que vraisemblable. Et il ajoute qu'en cas de problème cela révélerai surtout un bug dans le compilateur OCaml : ce qui est fort possible, il n'a pas été certifié.
Cela étant, il me semble que dans la famille des compilateurs C, seul CompCert est certifié et a résisté aux tests Csmith.
[^] # Re: Représentations intermédiaires du compilateur OCaml
Posté par kantien . En réponse au journal Malfunction: réutiliser la représentation intermédiaire du compilateur OCaml. Évalué à 1. Dernière modification le 26 juin 2016 à 22:25.
Ma réponse du dessous tombe à l'eau, maintenant. :-P
Cela montre surtout qu'il reste encore du travail à faire dessus, mais tout comme lui, sa conjecture me semble plus que vraisemblable. Et il ajoute qu'en cas de problème cela révélerai surtout un bug dans le compilateur OCaml : ce qui est fort possible, il n'a pas été certifié.
Cela étant, il me semble que dans la famille des compilateurs C, seul CompCert est certifié et a résisté aux tests Csmith.
Pour ce qui est de la famille des compilateurs de la famille ML, j'ai cru comprendre que Jacques Garrigue avait certifié certaines implémentations.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.