• [^] # Re: Performance

    Posté par . En réponse au journal Moi, expert C++, j'abandonne le C++. Évalué à 3.

    Ça tombe bien, personne n'a dit ça, et c'est une bêtise.

    Je crois que c'est moi qui l'est dit, et ce n'est pas une bêtise : c'est ce qu'offre les langages avec types dépendants. Du moins il dispense de tests unitaires, sauf pour ce qui est des erreurs dans la formalisation des spécifications du code.

    L'exemple le plus parlant est celui-ci :

    Theorem transform_c_programm_preservation :
 forall p tp beh
 transf_c_program p = Ok tp ->
 program_behaves (Asm.semantics tp) beh ->
 exists beh', programm_behaves (C.semantics p) beh'
 /\ behavior_improves beh' beh

    Laissant de côté le mot clef Theorem, le terme transform_c_programm_preservation est un terme du langage dont le type est l'énoncé exprimant que CompCert C est bien un compilateur C optimisant qui préserve la sémantique. Le terme, ou programme, est construit grâce à l'assistant de preuve Coq et il y a bien vérification statique qu'il a le bon type. Comme son type quantifie sur la totalité des programmes C (la varibale p du forall), qui est potentiellement infinie, il garantie des choses inaccessibles aux tests unitaires.

    Par contre, il reste la question : la formalisation de la sémantique de l'Asm (utilisée dans le terme Asm.semantics tp) est-elle conforme à la réalité ? Question dont la réponse est inaccessible aux méthodes formelles. De même pour ce qui est de la question sur la correction de la formalisation du C.

    Au niveau de la traduction en français, le type s'exprime ainsi : pour tout programme C p, tout programme assembleur tp et tout comportement observable beh, si la fonction transf_c_prgram appliquée à p renvoie le programme tp et que beh est un comportement observable de tp en accord avec la sémantique ASM, alors il existe un comportement observable beh' de p conforme à la sémantique du C et tel que beh améliore beh'.

    Autrement dit le type affirme que transf_c_program est un compilateur optimisant du C vers l'ASM.

    Ce cas extrême n'était pas pour inciter à l'usage des types dépendants, mais pour montrer que plus on introduit de typage statique et d'expressivité dans le système de types, moins on a besoin de tests unitaires (au point de ne plus en avoir besoin) : ce qui était bien ton propos initial. ;-)

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