Désolé si mon message a pu paraître agressif, telle n'était pas mon intention. C'est juste que je ne voyais pas où tu voulais en venir, ni le rapport avec les discussions du journal et des commentaires qu'il a suscités. Ma réaction était du même ordre que la fameuse réplique :
-- il dit qu'il a plus de genoux
-- il dit qu'il voit pas le rapport.
L'exemple central du journal tourne autour des garanties statiques que peut apporter Haskell (ou plus généralement, le système des ADT) pour la conception d'API et éviter les erreurs à l'exécution. S'en est suivi différentes discussions, avec des illustrations en ADA, Haskell ou OCaml, qui tournent toutes autour de ce même thème : peut-on (et si oui comment ?) contrôler la bonne formation des termes à la compilation (statiquement), ou doit-on mettre des gardes-fous et des tests lors de l'exécution (dynamiquement) ?
Ainsi lorsque je parlais d'outils d'analyses statiques, je ne considérais que ceux dont l'objectif se situe dans la gestion de cette problématique. C'est pour cela qu'à chacune de mes réponses, j'ai rappelé le contexte de la discussion. Je ne sous-entendais pas que les outils d'analyses de code se limitaient à gérer cette question. Et pour tous les cas d'usages que tu mentionnes, cela n'aurait d'ailleurs aucun sens d'avoir une alternative pour les traiter dynamiquement.
Une petite précision pour conclure :
Comme tu dis régulièrement que tu n'es pas développeur et que tu ne connais pas « l'industrie » ça ne me surprenait pas que tu ne connaisse pas ce pan là.
Il est vrai que je ne suis pas développeur (bien que je saches programmer, mais c'est loin d'être ma préoccupation première), et que je ne connais pas l'industrie. Mais quand je dis cela, c'est surtout pour exprimer que je ne sais pas ce qui est passé des laboratoires de recherche (et qui y est notoirement connu) vers le domaine industriel, ni le vocabulaire associé et le changement de dénomination qu'ont pu subir les notions lors du passage (ce qui est aussi parfois le cas lorsque la notion passe du domaine des mathématiques pures et de la logique à celui de l'informatique théorique).
Si je prends un exemple pour illustrer la chose. Dans la vidéo de la conférence sur JML (dont le lien était erroné, le voici), l'orateur expose sur un cas particulier une méthode d'analyse statique dite analyse polyédrique (vers la 40ème minute). Il conclue l'étude de cette exemple avec une diapo qui contient ce passage :
Principe de l'analyse de programme :
traduction vers un flux d'équation sur des ordres partiels
Les résultats de Tarski me sont connus depuis une bonne quinzaine d'années (époque où j'étais étudiant), et ce genre de conférence me permet de savoir que des industriels peuvent en faire usage (quant bien même ils ignoreraient ce qui se trouve sous le capot, ou dans quel contexte et pour quelles raisons ces problèmes ont été résolus à une époque où l'ordinateur n'existait pas encore).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Solution à base de types variants en ADA
Posté par kantien . En réponse à la dépêche Sortie de GHC 8.0.2 et une petite histoire de typage statique. Évalué à 3.
Désolé si mon message a pu paraître agressif, telle n'était pas mon intention. C'est juste que je ne voyais pas où tu voulais en venir, ni le rapport avec les discussions du journal et des commentaires qu'il a suscités. Ma réaction était du même ordre que la fameuse réplique :
L'exemple central du journal tourne autour des garanties statiques que peut apporter Haskell (ou plus généralement, le système des ADT) pour la conception d'API et éviter les erreurs à l'exécution. S'en est suivi différentes discussions, avec des illustrations en ADA, Haskell ou OCaml, qui tournent toutes autour de ce même thème : peut-on (et si oui comment ?) contrôler la bonne formation des termes à la compilation (statiquement), ou doit-on mettre des gardes-fous et des tests lors de l'exécution (dynamiquement) ?
Ainsi lorsque je parlais d'outils d'analyses statiques, je ne considérais que ceux dont l'objectif se situe dans la gestion de cette problématique. C'est pour cela qu'à chacune de mes réponses, j'ai rappelé le contexte de la discussion. Je ne sous-entendais pas que les outils d'analyses de code se limitaient à gérer cette question. Et pour tous les cas d'usages que tu mentionnes, cela n'aurait d'ailleurs aucun sens d'avoir une alternative pour les traiter dynamiquement.
Une petite précision pour conclure :
Il est vrai que je ne suis pas développeur (bien que je saches programmer, mais c'est loin d'être ma préoccupation première), et que je ne connais pas l'industrie. Mais quand je dis cela, c'est surtout pour exprimer que je ne sais pas ce qui est passé des laboratoires de recherche (et qui y est notoirement connu) vers le domaine industriel, ni le vocabulaire associé et le changement de dénomination qu'ont pu subir les notions lors du passage (ce qui est aussi parfois le cas lorsque la notion passe du domaine des mathématiques pures et de la logique à celui de l'informatique théorique).
Si je prends un exemple pour illustrer la chose. Dans la vidéo de la conférence sur JML (dont le lien était erroné, le voici), l'orateur expose sur un cas particulier une méthode d'analyse statique dite analyse polyédrique (vers la 40ème minute). Il conclue l'étude de cette exemple avec une diapo qui contient ce passage :
et la méthode de résolution (comme il le souligne à l'oral) est en partie fondée sur des travaux de Tarski qui datent des années 1930. Résultats auxquels j'avais fait allusion dans un autre journal. Ce type de technique se retrouve dans les solveurs SMT (Satisfiability modulo theories), comme par exemple l'outil alt-ergo (écrit en OCaml) utilisé, entre autre, par Spark dont a parlé Blackknight.
Les résultats de Tarski me sont connus depuis une bonne quinzaine d'années (époque où j'étais étudiant), et ce genre de conférence me permet de savoir que des industriels peuvent en faire usage (quant bien même ils ignoreraient ce qui se trouve sous le capot, ou dans quel contexte et pour quelles raisons ces problèmes ont été résolus à une époque où l'ordinateur n'existait pas encore).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.