ça a de grosses conséquances sur la génération de code sûr (au sens de la sûreté de fonctionnement) pour des missions critiques comme les codes embarquées par exemple. Les autres méthodes de code sûr pour ce genre de tâches (Lustre et Esterel pour ne pas les citer) ont d'autres avantages mais ne servent jamais qu'à générer du code C à recompiler derrière.
Oui, Ada n'a pas de définition formelle, mais c'est quand même un des rares langages dont la définition soit à la fois suffisement complète et non ambigu pour que l'on puisse en extraire des sous-ensemble prouvable formellement, sans dépendance au compilateur.
Pour les autres langage de ce type, les outils doivent compenser les trous de sémantiques de la définition du langage par la connaissance du comportement constaté du compilateur. C'est vrai par exemple, même pour un sous-ensemble de C comme MISRA-C, pourtant spécifiquement dédié à ces applications critiques.
[^] # Re: Ada answers
Posté par Lionel Draghi (site web personnel) . En réponse à la dépêche Langages et performances : les Français à l'honneur !. Évalué à 2.
Oui, Ada n'a pas de définition formelle, mais c'est quand même un des rares langages dont la définition soit à la fois suffisement complète et non ambigu pour que l'on puisse en extraire des sous-ensemble prouvable formellement, sans dépendance au compilateur.
Pour les autres langage de ce type, les outils doivent compenser les trous de sémantiques de la définition du langage par la connaissance du comportement constaté du compilateur. C'est vrai par exemple, même pour un sous-ensemble de C comme MISRA-C, pourtant spécifiquement dédié à ces applications critiques.
Si celà t'intéresse, actuellement un produit original nomé SPARK fait une percée remarquée dans le monde de la preuve formelle Ada : http://www.praxis-his.com/sparkada/intro.asp(...)
Quoi qu'il en soit, le marché des applis embarqués critiques est justement LE marché dominé par Ada.