La démonstration formelle que l'application X (genre le contrôleur des moteurs de l'avion ne crachera pas). Je sais que Coq (ou des outils similaires) ont été utilisé dans ce genre de contexte. Mais que cela reste réservé à ce niveau de criticité et pour des logiciels assez petits.
Bien sûr, je connais, j'ai bossé dans le milieu (DAL C au plus haut). Mais tu n'as pas besoin d'aller si loin que ce que kantien annonce à savoir démontrer par les maths que ton système va marcher à tous les coups.
D'ailleurs pour les DAL >= C, il devient difficile d'employer des CPU multi-cœurs ou avec un GPU moderne tellement que c'est contraignant vis à vis des normes. Donc imaginer démontrer avec Coq que Linux tourne bien sur le dernier Intel couplé avec un GPU nVidia, on en est très très loin.
[^] # Re: Le cerveau n'est pas logique
Posté par Renault (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
La démonstration formelle que l'application X (genre le contrôleur des moteurs de l'avion ne crachera pas). Je sais que Coq (ou des outils similaires) ont été utilisé dans ce genre de contexte. Mais que cela reste réservé à ce niveau de criticité et pour des logiciels assez petits.
Bien sûr, je connais, j'ai bossé dans le milieu (DAL C au plus haut). Mais tu n'as pas besoin d'aller si loin que ce que kantien annonce à savoir démontrer par les maths que ton système va marcher à tous les coups.
D'ailleurs pour les DAL >= C, il devient difficile d'employer des CPU multi-cœurs ou avec un GPU moderne tellement que c'est contraignant vis à vis des normes. Donc imaginer démontrer avec Coq que Linux tourne bien sur le dernier Intel couplé avec un GPU nVidia, on en est très très loin.