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

    Posté par (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.

    Le typage statique est un tel outil. La plupart des systèmes de types n'évitent pas la nécessité de recourir à des tests unitaires, mais ils permettent de capturer certaines erreurs de raisonnement.

    Le problème est que tu n'attrapes pas grand chose comme erreur avec un système de typage. La seul architecture que j'ai trouvé pour aider est de transformer un arbre en un autre, sans aucune information redondante ni inutile. Ainsi, un mauvais usage ne compile pas, et on ne traine pas l'entrée à l'intérieur du code. Cela marche bien dans les "filtres unix" mais dans rien d'autre, pour des raisons de performances si les données sont énormes ou pour des raisons pratiques comme l'optimisation d'un AST qui doit donner aussi un AST.

    Si on regarde le gadt, la complexité est encore plus grande sans réellement attraper une énorme quantité de bugs supplémentaires. En gros, la complexité devient exponentielle, pour attraper des bugs de façon linéaire.

    J'ai discuté avec l'auteur français de smarteffel(?), qui utilise beaucoup les contrats, il disait qu'en codant, il violait régulièrement même des contrats de base présent dans les containers, car la pile d’héritage en bénéficiait (les contrats n’héritent). C'était d'une grande aide pour lui.

    Le problème est que le contrat est runtime et nécessite un test pour s’exercer. Il n'est pas possible d'avoir des contrats compile-time ou de vérifier leur cohérence entre eux ?

    "La première sécurité est la liberté"