Un commentaire pour ajouter des compléments de lecture à ton article tests vs types, qui est relatif aux questions : comment définir les spécifications d'un code ? et comment être certain que le code répond bien à ses spécifications ?
Comme l'article auquel tu renvoies traite de Haskell et de Idris (du ML made in England), il y a l'équivalent made in France. Dans un ancien journal Qui fait des trucs "cool" en France et en Europe ?, j'avais essayé d'expliquer les principes à la base de la différence entre OCaml et Coq et pourquoi le système de types du second permet de se dispenser des tests unitaires.
Au passage, comme tu abordes aussi la question des gestionnaires de paquets, OCaml dispose du sien : opam dont l'architecture est basé sur les résultats de recherches du projet Mancoosi (qui a aussi servie au projet Debian pour son assurance qualité), en particulier sur la nature NP-complet du problème de gestion des dépendances.
Last but not least, en rapport avec la compilation clojure vers du bytecode JVM, la machine virtuelle Coq (qui est LE langage fonctionnelle le mieux typé) a été compilé en javascript via OBrowser (et tourne donc dans un navigateur) par une start-up française : edukera.
P.S : le journal de Big Pete renvoie a une leçon en cours sur les réseaux neuronaux convolutionnels qui permettent, en autre, de faire de la reconnaissance d'images. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
# Tests vs Types
Posté par kantien . En réponse au journal De tout, de rien, des bookmarks, du bla bla. Évalué à 3.
Un commentaire pour ajouter des compléments de lecture à ton article tests vs types, qui est relatif aux questions : comment définir les spécifications d'un code ? et comment être certain que le code répond bien à ses spécifications ?
Un journal récent de Big Pete m'a rappelé les excellents cours de Gérard Berry au Collège de France. Sur le sujet en question, il y a tout le cours de l'année 2014-2015 : Prouver les programmes : pourquoi, quand, comment ? ou celui de cette année structures de données et algorithmes pour la vérification formelle (la première leçon et le séminaire qui suit est une bonne présentation, avec des exemples en Java et intégration dans les commentaires du code).
Comme l'article auquel tu renvoies traite de Haskell et de Idris (du ML made in England), il y a l'équivalent made in France. Dans un ancien journal Qui fait des trucs "cool" en France et en Europe ?, j'avais essayé d'expliquer les principes à la base de la différence entre OCaml et Coq et pourquoi le système de types du second permet de se dispenser des tests unitaires.
Au passage, comme tu abordes aussi la question des gestionnaires de paquets, OCaml dispose du sien : opam dont l'architecture est basé sur les résultats de recherches du projet Mancoosi (qui a aussi servie au projet Debian pour son assurance qualité), en particulier sur la nature NP-complet du problème de gestion des dépendances.
Last but not least, en rapport avec la compilation clojure vers du bytecode JVM, la machine virtuelle Coq (qui est LE langage fonctionnelle le mieux typé) a été compilé en javascript via OBrowser (et tourne donc dans un navigateur) par une start-up française : edukera.
P.S : le journal de Big Pete renvoie a une leçon en cours sur les réseaux neuronaux convolutionnels qui permettent, en autre, de faire de la reconnaissance d'images. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.