Posté par newca .
En réponse à la dépêche [code] Trouver les erreurs.
Évalué à 9.
Dernière modification le 14 janvier 2015 à 23:22.
L'erreur est humaine et les tests unitaires ne sont (presque) jamais exhaustifs, il existe fort heureusement d'autres approches.
LA PREUVE DE PROGRAMME !
Il est sans doute intéressant de rappeler comment le gars qui a trouvé la faille SSL a procédé :
Le gars a utilisé Coq un puissant assistant de preuve (mathématiques) pour "révéler" le bug.
La méthode qu'il a employée est tout simplement fantastique : http://ccsinjection.lepidum.co.jp/blog/2014-06-05/CCS-Injection-en/index.html#how-did-i-discover-the-bug
Clairement c'est le genre de gars qui ouvre la voie pour démocratiser la démonstration de programme.
Pour ceux que çà intéresse un cours bien fait sur le sujet (orienté Coq) : http://fuscia.inrialpes.fr/cours/coq/
Bien sûr il est irréaliste de vouloir développer un programme d'envergure en Coq mais ces techniques commence à être disponibles sur des langages "mainstream".
Leon (http://lara.epfl.ch/w/leon) par exemple est très prometteur pour démontrer du code en Scala.
# Une autre approche est possible
Posté par newca . En réponse à la dépêche [code] Trouver les erreurs. Évalué à 9. Dernière modification le 14 janvier 2015 à 23:22.
L'erreur est humaine et les tests unitaires ne sont (presque) jamais exhaustifs, il existe fort heureusement d'autres approches.
LA PREUVE DE PROGRAMME !
Il est sans doute intéressant de rappeler comment le gars qui a trouvé la faille SSL a procédé :
Le gars a utilisé Coq un puissant assistant de preuve (mathématiques) pour "révéler" le bug.
La méthode qu'il a employée est tout simplement fantastique : http://ccsinjection.lepidum.co.jp/blog/2014-06-05/CCS-Injection-en/index.html#how-did-i-discover-the-bug
Clairement c'est le genre de gars qui ouvre la voie pour démocratiser la démonstration de programme.
Pour ceux que çà intéresse un cours bien fait sur le sujet (orienté Coq) : http://fuscia.inrialpes.fr/cours/coq/
Bien sûr il est irréaliste de vouloir développer un programme d'envergure en Coq mais ces techniques commence à être disponibles sur des langages "mainstream".
Leon (http://lara.epfl.ch/w/leon) par exemple est très prometteur pour démontrer du code en Scala.
Mais il existe tout un tas d'outils et d'approches pour vérifier/démontrer qu'un programme est correct : https://github.com/johnyf/tool_lists/blob/master/verification_synthesis.md
IMHO c'est çà l'avenir de l'informatique et c'est par ce biais que ce fera la jonction (naturelle) avec les mathématiques !
Tous les développeurs devraient s'intéresser à la preuve de programme et pas seulement les universitaires ou les boites spécialisées.