compcert a été prouvé avec seulement ce bout de code ? Sans rien de manuel ?
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". De plus la preuve formelle n'est pas encore reconnu dans les certifications aéronautique, en tout cas dans la do178b, je crois que cela bouge un peu dans la DO178C. Et encore, j'imagine que le prouveur lui-même devrait être certifié... Donc, on est pas prêt de voir un avion volé avec un tel code sans certification "papier" à coté. L'outil de ma boite utilisait l'outil de prover, mais c'était peu/aps utilisé car la norme n'en voulait pas.
Pour le reste des échanges, j'arrête là : je pisse dans un violon, tu ne connais pas grand chose aux sujets abordés mais tu parles quand même, ça me saoule.
Je crois que je peux te répondre la même chose, mais pas pour le même domaine.
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
compcert a été prouvé avec seulement ce bout de code ? Sans rien de manuel ?
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". De plus la preuve formelle n'est pas encore reconnu dans les certifications aéronautique, en tout cas dans la do178b, je crois que cela bouge un peu dans la DO178C. Et encore, j'imagine que le prouveur lui-même devrait être certifié... Donc, on est pas prêt de voir un avion volé avec un tel code sans certification "papier" à coté. L'outil de ma boite utilisait l'outil de prover, mais c'était peu/aps utilisé car la norme n'en voulait pas.
Je crois que je peux te répondre la même chose, mais pas pour le même domaine.
"La première sécurité est la liberté"