C'est plus difficile. Dans le domaine du hardware les domaines d'entrée sont finis (des bus de N bits) et se prêtent très bien à la vérification automatique (grosses formules SAT, etc.). Dans le domaine du software les domaines d'entrées sont plus compliqués ("une URL", "un fichier JPEG"), et les logiques plus compliquées.
La communauté du hardware est très en avance culturellement à cause du coût des erreurs. La communauté software, et en particulier la communauté du logiciel libre, est en retard sur l'adoption d'outils de vérification.
On commence à avoir des outils pour prouver que deux programmes sont équivalents, mais en général de façon non-automatique. C'est utilisée par exemple comme une façon de faire des preuves de correction : tu écris un programme efficace/optimisé que tu veux utiliser en production, et un programme simple et naïf que tu utilises comme "spécification" (ou implémentation de référence), et tu essaies de montrer qu'ils sont équivalents.
P.S.: Il y a un exception notable, qui est le test d'équivalence entre deux automates. Il y a des outils pour faire ça qui sont utilisés dans certaines communautés (en fait on teste plus souvent le vide, le fait qu'un automate accepte au moins une entrée, mais les deux problèmes sont proches). On peut voir les automates (à état finis, à pile, à poil ras, etc.) comme des cas particuliers de programmes très contraints avec de bonne propriétés—une partie des outils de Model Checking utilise ces idées, par exemple.
[^] # Re: Perl6
Posté par gasche . En réponse au journal La recherche en langages de programmation au quotidien. Évalué à 7.
Non, et il y a au moins deux raisons :
C'est plus difficile. Dans le domaine du hardware les domaines d'entrée sont finis (des bus de N bits) et se prêtent très bien à la vérification automatique (grosses formules SAT, etc.). Dans le domaine du software les domaines d'entrées sont plus compliqués ("une URL", "un fichier JPEG"), et les logiques plus compliquées.
La communauté du hardware est très en avance culturellement à cause du coût des erreurs. La communauté software, et en particulier la communauté du logiciel libre, est en retard sur l'adoption d'outils de vérification.
On commence à avoir des outils pour prouver que deux programmes sont équivalents, mais en général de façon non-automatique. C'est utilisée par exemple comme une façon de faire des preuves de correction : tu écris un programme efficace/optimisé que tu veux utiliser en production, et un programme simple et naïf que tu utilises comme "spécification" (ou implémentation de référence), et tu essaies de montrer qu'ils sont équivalents.
P.S.: Il y a un exception notable, qui est le test d'équivalence entre deux automates. Il y a des outils pour faire ça qui sont utilisés dans certaines communautés (en fait on teste plus souvent le vide, le fait qu'un automate accepte au moins une entrée, mais les deux problèmes sont proches). On peut voir les automates (à état finis, à pile, à poil ras, etc.) comme des cas particuliers de programmes très contraints avec de bonne propriétés—une partie des outils de Model Checking utilise ces idées, par exemple.