Ce n'est pas aussi simple. Compcert est un compilateur pensé pour du code qui s'exécute dans des systèmes critiques, code qui lui-même a été analysé de mille façons pour s'assurer qu'il n'a pas de bugs en soi. Il apporte une garantie très agréable pour ce genre de logiciels. Mais dans le contexte d'un compilateur pour tout un OS assez généraliste, même avec certaines priorités, la plupart du code n'a pas pu, ne peut pas, se permettre autant de perfection, et du coup n'entre pas dans le cadre visé. En pratique, ça signifie par exemple que la version patchée de gcc dans OpenBSD utilise des méthodes pour faire en sorte que les failles dans du code buggué ne soient pas si facilement exploitables. Si tu remplaces le gcc actuel, puis que tu compiles tout OpenBSD avec Compcert (si c'est vraiment possible), c'est pas sûr que le résultat sera plus sûr, en fin de compte : pour cela il faudrait que les programmes n'aient pas de bugs.
Bref, ce qui serait bien c'est un compilateur libre écrit avec l'objectif d'être suffisamment correct, mais utilisé pour tout un OS, ce qui inclut compiler du code avec des bugs et faire en sorte qu'ils soient moins gênants ou les détecter si c'est possible, mais aussi des bons messages d'erreurs, génération de code pour suffisamment d'architectures, pas trop mais suffisamment optimisant (sachant que les applications d'OpenBSD sont quand même variées), et suffisamment rapide, car je pense que le temps de compilation a bien une importance : le code d'OpenBSD, ainsi que l'ensemble des ports, est en train de se compiler en permanence, il me semble, du coup si tu doubles le temps de compilation, tu ralentis le procédé et, même avec plus de machines, tu augmenterais au moins la facture d'électricité... Le fait est, qu'actuellement, ce qui s'approche le plus d'un tel compilateur semble être le gcc patché d'OpenBSD.
[^] # Re: Compilateur sans bugs
Posté par anaseto . En réponse à la dépêche OpenBSD 5.7 « Blues Brothers ». Évalué à 7.
Ce n'est pas aussi simple. Compcert est un compilateur pensé pour du code qui s'exécute dans des systèmes critiques, code qui lui-même a été analysé de mille façons pour s'assurer qu'il n'a pas de bugs en soi. Il apporte une garantie très agréable pour ce genre de logiciels. Mais dans le contexte d'un compilateur pour tout un OS assez généraliste, même avec certaines priorités, la plupart du code n'a pas pu, ne peut pas, se permettre autant de perfection, et du coup n'entre pas dans le cadre visé. En pratique, ça signifie par exemple que la version patchée de gcc dans OpenBSD utilise des méthodes pour faire en sorte que les failles dans du code buggué ne soient pas si facilement exploitables. Si tu remplaces le gcc actuel, puis que tu compiles tout OpenBSD avec Compcert (si c'est vraiment possible), c'est pas sûr que le résultat sera plus sûr, en fin de compte : pour cela il faudrait que les programmes n'aient pas de bugs.
Bref, ce qui serait bien c'est un compilateur libre écrit avec l'objectif d'être suffisamment correct, mais utilisé pour tout un OS, ce qui inclut compiler du code avec des bugs et faire en sorte qu'ils soient moins gênants ou les détecter si c'est possible, mais aussi des bons messages d'erreurs, génération de code pour suffisamment d'architectures, pas trop mais suffisamment optimisant (sachant que les applications d'OpenBSD sont quand même variées), et suffisamment rapide, car je pense que le temps de compilation a bien une importance : le code d'OpenBSD, ainsi que l'ensemble des ports, est en train de se compiler en permanence, il me semble, du coup si tu doubles le temps de compilation, tu ralentis le procédé et, même avec plus de machines, tu augmenterais au moins la facture d'électricité... Le fait est, qu'actuellement, ce qui s'approche le plus d'un tel compilateur semble être le gcc patché d'OpenBSD.