Tout d'abord, je tiens à dire que je ne programme quasiment pas mais j'enseigne la programmation et je corrige des projets d'étudiants. En ce moment, j'enseigne un module de preuve de programme. Ce n'est pas un module de très haut niveau. C'est du L2 mais je le trouve très intéressant.
En effet, même si au final, on ne prouve pas réellement son code, écrire comme si on allait le faire pousse à écrire plus proprement pour plusieurs raison.
1. pour prouver un code, il faut savoir pourquoi il ne plante pas. On peut ainsi documenter les variants et invariants de boucles. On peut spécifier le comportement des fonctions qu'on écrit. Bref, on peut documenter le code et ça rend la relecture plus simple.
2. prouver, c'est chiant et c'est long. Garder une structure globale simple simplifie beaucoup le boulot.
# Avis d'un théoricien
Posté par fmaz fmaz . En réponse au journal Du code propre, c'est quoi ?. Évalué à 10.
Tout d'abord, je tiens à dire que je ne programme quasiment pas mais j'enseigne la programmation et je corrige des projets d'étudiants. En ce moment, j'enseigne un module de preuve de programme. Ce n'est pas un module de très haut niveau. C'est du L2 mais je le trouve très intéressant.
En effet, même si au final, on ne prouve pas réellement son code, écrire comme si on allait le faire pousse à écrire plus proprement pour plusieurs raison.
1. pour prouver un code, il faut savoir pourquoi il ne plante pas. On peut ainsi documenter les variants et invariants de boucles. On peut spécifier le comportement des fonctions qu'on écrit. Bref, on peut documenter le code et ça rend la relecture plus simple.
2. prouver, c'est chiant et c'est long. Garder une structure globale simple simplifie beaucoup le boulot.
Bref.