L’emploi de la preuve garantit qu’il n’y aura pas de distorsion entre le modèle mathématique initial, issu de la spécification écrite en français, et le modèle mathématique final, extrêmement proche du code exécutable. Mais, en deçà et au-delà, rien n’est garanti par la preuve. Si, par exemple, la spécification en français est erronée ou si le modèle mathématique initial n’est pas fidèle à cette spécification, on sort des limites de l’épure. De même, si le traducteur qui transforme le dernier modèle mathématique en code ou si le compilateur qui le traduit en code binaire sont bogués, on ne peut rien garantir. Le zéro défaut absolu n’existe pas. Mais on peut s’en approcher toujours plus. Ce que l’on peut faire avec une méthode formelle va certainement beaucoup plus loin que ce que lon peut garantir avec des tests unitaires. Mais il ne faut pas croire que le problème est résolu dans son ensemble : le retour de bâton serait terrible.
👉🏻 Suivez l’actualité tech en temps réel : ajoutez 01net à vos sources sur Google, et abonnez-vous à notre canal WhatsApp.
