• [^] # Re: Le cerveau n'est pas logique

    Posté par . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4. Dernière modification le 20 octobre 2017 à 14:34.

    Le problème est que tu n'attrapes pas grand chose comme erreur avec un système de typage.

    Et les licornes roses ont de jolies ailes ! :-D

    Tu te rends compte de ce que tu viens d'écrire ? D'une la quantité d'erreurs attrapées à la compilation dépend de l'expressivité du système de types, et de deux on peut pousser le système jusqu'à permettre de se dispenser totalement de tests unitaires. Exemple :

    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

    Traduction en français : 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 : la fonction transform_c_program est un compilateur optimisé du C vers l'assembleur préservant la sémantique du code source et certifié conforme ! Pas besoin de faire de tests unitaires : quand dans l'énoncé on quantifie sur tous les programmes et tous les comportements, on parle bien de l'infinité des programmes et des comportements possibles (on ne peut pas faire des tests unitaires sur une infinité de cas). :-)

    Tu noteras au passage la notation transform_c_programm_preservation : blabla où blabla est tout à la fois le type et l'énoncé du théorème. ;-)

    Plus de détails et de compléments dans la vidéo In search of software perfection - 2016 Milner Award lecture by Dr Xavier Leroy..

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