The Coq mailing list

["Marc Daumas" <Marc.Daumas AT ENS-Lyon.Fr>]

> Objet : [Coq-Club] Post-Doc Announcement at INRIA and CNAM-IIE (France)
...
> L'action de recherche cooperative "Concert" à l'INRIA propose une
> bourse doctorale pour les étudiants intéressés dans la formalisation
> et la certification de compilateurs optimisant pour des langages de
> programmation généralistes de la famille du langage C.  L'objectif
> initial est d'effectuer cette formalisation et cette certification
> dans le cadre du calcul des constructions inductives (le système Coq),
> afin de tirer parti des caractèristiques de ce système pour la
> production de logiciel certifié, par exemple à l'aide du mécanisme
> d'extraction.
...
> http://www-sop.inria.fr/lemme/concert/

Bonjour,

Utilisateurs de Coq, nous sommes bien évidemment très intéressés par le
futur de l'action Concert. Je voudrais toutefois préciser les points
suivants:

1 - Il est impossible d'identifier les nombres à virgule flottante avec une
sous structure des réels. Stricto sensu, cela empêche tout changement dans
l'ordre des opérations et toute optimisation sur les expressions à virgule
flottante. La question est par exemple soulevée dans la seconde édition du
Kernighan et Ritchie (1990), page 199 dans l'édition de Masson en français.
En pratique, les compilateurs se donnent quelques libertés. Il faudrait se
demander ce que ces libertés signifient au niveau de la qualité des calculs.
Avec l'utilisation de machines de plus en plus superscalaires (IA64) il
semble hors de question que les concepteurs de compilateurs renoncent à ces
optimisations.

2 - Selon les machines, certaines opérations à virgule flottante sont
implantées en matériel ou en logiciel. Dans le second cas, il faut avoir
certifié le bon fonctionnement des bibliothèques s'il on veut pouvoir
certifier le fonctionnement de tout programme utilisant un tant soit peu de
trigonométrie (par exemple, le positionnement d'un point sur terre à partir
de sa latitude et de sa longitude).

3 - La certification d'un compilateur idéalisé est une étape obligatoire
mais la route est longue jusqu'à la certification d'un produit finalisé. Il
serait trop bête de tomber dans un piège de l'unité de calcul à virgule
flottante tel que celui de la limitation de la pile des machines Intel IA32
(cf http://grouper.ieee.org/groups/754/meeting-minutes/02-07-18.html).

N'hésitez pas à tenir la liste coq-club informée de vos travaux.

Sincèrement,

--
Marc Daumas - Charge de recherches au CNRS (LIP - ENS de Lyon)
mailto:Marc.Daumas AT ENS-Lyon.Fr
 - http://www.ens-lyon.fr/~daumas
PGP Key FP : 69B6 11D1 DA61 717F DF76  5B92 E4EC B289 D607 F324
ENS de Lyon - 46, allee d'Italie - 69364 Lyon Cedex 07 - FRANCE
Phone: (+33) 4 72 72 85 83 - Fax: (+33) 4 72 72 80 80