Concernant Astrée, j'imagine que c'est le genre d'outil qui peut généré un paquet de faux positif. Par exemple, si il détecte trop "simplement" la division. Sparse ne génère pas de faux positif si je me rappelle bien. Si il ne fonctionne bien qu'avec un code généré par SCADE, il y a une gros soucis (sachant que SCADE génère un C restreint ayant déjà beaucoup de bonnes propriétés).
Coverity propose une analyse de code open source. ( https://www.synopsys.com/software-integrity/resources/analyst-reports/open-source-software-scan-report.html ) Cela a été à la mode pendant un moment, puis les devs en ont eu marre des faux positifs dont la corrections pouvaient entrainée des problèmes subtiles (genre générateur de nombre aléatoire de Debian). Je ne connais pas la différence avec Astrée, mais Sparse a été développé ensuite.
Encore une fois, pour ça il faut une culture volontaire du côté des développeurs, et elle manque pour le noyau Linux (alors qu'elle est présente pour Windows, en partie parce que Microsoft n'a pas laissé le choix à ses développeurs).
Le milieu Open Source ne fonctionne pas comme ça. Celui qui apporte une nouvelle techno doit démontrer sa supériorité pour convaincre. Dire "venez avec moi, cela va être génial", cela fait 20 ans, que les développeurs Kernel l'entendent tous les jours. Et au dernière nouvelles les drivers Windows ne fonctionnent pas mieux que les drivers Linux.
En gros, c'est à la communauté de la recherche de prouver que leur approche est meilleur, si vous considérez que les dev sont bêtes parce qu'ils ne vous écoutent pas, c'est mal barré.
Par exemple le code pour décrire une multiplication matrice/vecteur (GEMV en BLAS) dans ce langage est
L'idée est sympa. J'imagine que les usagers de ce genre de DSL sont docteur en mathématique pour le calcul linéaire. Je ne vois pas qui d'autres pourraient s'en servir vu le formalisme mathématique retenu.
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 5.
Concernant Astrée, j'imagine que c'est le genre d'outil qui peut généré un paquet de faux positif. Par exemple, si il détecte trop "simplement" la division. Sparse ne génère pas de faux positif si je me rappelle bien. Si il ne fonctionne bien qu'avec un code généré par SCADE, il y a une gros soucis (sachant que SCADE génère un C restreint ayant déjà beaucoup de bonnes propriétés).
Coverity propose une analyse de code open source. ( https://www.synopsys.com/software-integrity/resources/analyst-reports/open-source-software-scan-report.html ) Cela a été à la mode pendant un moment, puis les devs en ont eu marre des faux positifs dont la corrections pouvaient entrainée des problèmes subtiles (genre générateur de nombre aléatoire de Debian). Je ne connais pas la différence avec Astrée, mais Sparse a été développé ensuite.
Le milieu Open Source ne fonctionne pas comme ça. Celui qui apporte une nouvelle techno doit démontrer sa supériorité pour convaincre. Dire "venez avec moi, cela va être génial", cela fait 20 ans, que les développeurs Kernel l'entendent tous les jours. Et au dernière nouvelles les drivers Windows ne fonctionnent pas mieux que les drivers Linux.
En gros, c'est à la communauté de la recherche de prouver que leur approche est meilleur, si vous considérez que les dev sont bêtes parce qu'ils ne vous écoutent pas, c'est mal barré.
L'idée est sympa. J'imagine que les usagers de ce genre de DSL sont docteur en mathématique pour le calcul linéaire. Je ne vois pas qui d'autres pourraient s'en servir vu le formalisme mathématique retenu.
"La première sécurité est la liberté"