compcert a été prouvé avec seulement ce bout de code ? Sans rien de manuel ?
Bien sur que non, c'est un travail de titan le code complet ! C'était pour illustrer ma proposition « la quantité d'erreurs attrapées à la compilation dépend de l'expressivité du système de types », en montrant un système de types tel que son expressivité dispense d'avoir à recourir à des tests unitaires. Ce théorème, qui n'est qu'une infime partie du code du compilateur, est celui que Xavier Leroy utilise dans sa vidéo comme illustration : c'est normal, c'est lui qui exprime que son compilateur est optimisant est n'apporte aucune modification de comportement à la compilation (si il y a un problème dans le code compilé, il se trouve déjà dans le code C).
Pour info, j'ai bossé 10 ans dans l'aéronautique, et l'usage des compilos C certifié c'était plutôt : "il faudrait prendre le temps de voir ce que cela donne".
Je le sais bien, c'est pour cela que j'ai parlé de cette industrie. Au sujet du projet CompCert C, Gérard Berry (lui, tu le connais il a cofondé l'entrepise qui fut (est ?) ton employeur et est le père du langage Esterel) l'a décrit dans le bulletin de la société informatique de France ainsi :
CompCert, l’autre grande contribution de Xavier Leroy et de son équipe, est une aventure encore unique sur le plan mondial. Il s’est agi de réaliser un compilateur du langage C qui soit non plus certifié seulement pour la qualité des méthodes de développement et de test comme dans la norme DO-178C, mais bel et bien prouvé mathématiquement correct et donc vraiment garanti sans bugs.
Pour info le compilateur est un produit (il n'est pas libre, seulement pour un usage non-commercial) de l'entreprise AbstInt :
Certification and qualification
Current safety standards such as ISO 26262, DO-178B/C, IEC-61508, EN-50125 and others require identifying potential functional and non-functional hazards and demonstrating that the software does not violate the relevant safety goals.
Abstract-interpretation based tools such as aiT, StackAnalyzer, and Astrée provide formal verification with 100% complete and reliable results. They are therefore perfectly suited to be used for certification.
The qualification process is greatly simplified by our Qualification Support Kits. Additionally, Qualification Software Life Cycle Data Reports provide details about our development processes.
qui a pour client Airbus et pour partenaire Esterel Technologies. ;-) Pour Airbus, ils utilisent leurs analyseurs statiques de code (aiT analyse le comportement temporel, StackAnalyzer l'absence de stack overflow et Astrée l'absence de runtime error) :
For many years Airbus France has been using aiT, StackAnalyzer and Astrée in the development of safety-critical avionics software for several airplane types, including the A380, the world’s largest passenger aircraft. The analyzers are used as part of certification strategy to demonstrate compliance to DO-178B, up to Level A.
et Compert C s'incrit dans la chaîne des outils : si le code C est propre et garanti c'est bien, mais si le compilateur introduit un bug c'est un peu couillon, tu ne crois pas ?
Je crois que je peux te répondre la même chose, mais pas pour le même domaine.
T'es sûr ? Tu faisais (ou fais) quoi comme travail chez Esterel ? Tu y appris quoi chez eux pour avoir écrit cela ?
Les exemples de preuve sont très matheux. Cela ne ressemble pas à des preuves "industrielles" (à base de bout de spec, de bout d'exemple, de ne "plante jamais", a un temps d'exécution borné).
T'as pas compris depuis le temps que ce tu qualifies de "industrielles", ce sont aussi des preuves de matheux ? ;-)
Tu devrais tout de même jeter un œil à la vidéo de Xavier Leroy dont j'ai donné le lien au-dessus, il y parle pendant une vingtaine de minutes du milieu de l'avionique et de ses exigences de certification.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le cerveau n'est pas logique
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4. Dernière modification le 21 octobre 2017 à 00:41.
Bien sur que non, c'est un travail de titan le code complet ! C'était pour illustrer ma proposition « la quantité d'erreurs attrapées à la compilation dépend de l'expressivité du système de types », en montrant un système de types tel que son expressivité dispense d'avoir à recourir à des tests unitaires. Ce théorème, qui n'est qu'une infime partie du code du compilateur, est celui que Xavier Leroy utilise dans sa vidéo comme illustration : c'est normal, c'est lui qui exprime que son compilateur est optimisant est n'apporte aucune modification de comportement à la compilation (si il y a un problème dans le code compilé, il se trouve déjà dans le code C).
Je le sais bien, c'est pour cela que j'ai parlé de cette industrie. Au sujet du projet CompCert C, Gérard Berry (lui, tu le connais il a cofondé l'entrepise qui fut (est ?) ton employeur et est le père du langage Esterel) l'a décrit dans le bulletin de la société informatique de France ainsi :
Pour info le compilateur est un produit (il n'est pas libre, seulement pour un usage non-commercial) de l'entreprise AbstInt :
qui a pour client Airbus et pour partenaire Esterel Technologies. ;-) Pour Airbus, ils utilisent leurs analyseurs statiques de code (aiT analyse le comportement temporel, StackAnalyzer l'absence de stack overflow et Astrée l'absence de runtime error) :
et Compert C s'incrit dans la chaîne des outils : si le code C est propre et garanti c'est bien, mais si le compilateur introduit un bug c'est un peu couillon, tu ne crois pas ?
T'es sûr ? Tu faisais (ou fais) quoi comme travail chez Esterel ? Tu y appris quoi chez eux pour avoir écrit cela ?
T'as pas compris depuis le temps que ce tu qualifies de "industrielles", ce sont aussi des preuves de matheux ? ;-)
Tu devrais tout de même jeter un œil à la vidéo de Xavier Leroy dont j'ai donné le lien au-dessus, il y parle pendant une vingtaine de minutes du milieu de l'avionique et de ses exigences de certification.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.