• [^] # Re: Nuance

    Posté par . En réponse au journal Xavier Leroy est le lauréat 2016 du Prix Milner.. Évalué à 3.

    Les erreurs semblent bien avoir été corrigées. Au moins pour celle sur la signature du la fonction main d'après le manuel datant du 30 juin 2016 :

    The following limitations apply to the C source files that can be interpreted.

    1. [...]
    2. [...]
    3. The main function must be declared with one of the two types allowed by the C standards, namely:
    int main(void) { ... }
int main(int argc, char ** argv) { ... }

    Par contre, je ne comprends pas ce que tu entends par réaliste lorsque tu dis : « je ne cherche pas à dire que les spécifications de CompCert sont fausses, seulement qu'on ne peut pas savoir si elles sont complètes et réalistes ». Que l'on se demande si les spécifications d'un langage sont correctes et complètes (ou plutôt leur formalisation dans un autre langage), je peux le comprendre (et il n'est pas possible de le prouver formellement non plus, la question ne portant pas sur la forme mais sur la matière ou le contenu). Mais se demander si elles sont réalistes n'a aucun sens.

    Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.