Il y a un bug trivial dans le compilateur formellement vérifié de l'INRIA
https://twitter.com/johnregehr/status/943150088544591874 …
Je ne comprends pas ta réponse. Le projet est hébergé sur compcert[.]inria[.]fr depuis les origines (2008). C'est une équipe de recherche qui travaille en sous-marin, sans l'accord de leur direction ?
-
-
Une manière dont CompCert est le projet d'un chercheur plutôt que d'Inria, c'est que quand XL a commencé de travailler dessus, Inria n'a pas même été au courant avant qu'il ne fournisse sa contribution au rapport annuel suivant.
-
A contrario, s'il prend la décision personnelle de faire autre chose, il n'y a plus de CompCert. En fait ça ce n'est pas tout à fait vrai, il y a d'autres chercheurs qui contribuent maintenant. Pas nécessairement Inria.
- 5 more replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.