BookeldOr (./22) :
C'était juste pour dire (de manière certes trollatoire) que parfois on peut être certain d'appeler une fonction avec la bonne valeur partout dans son code et que mettre ces vérifications à la Hoare à la main partout n'est pas forcément nécessaire et parfois ne fait que polluer le code et le rendre illisible avec un tas d'assertions partout.
Par exemple, on peut très bien passer une analyse statique ensuite qui vérifie, pour te faire plaisir avec une sémantique axiomatique, que les valeurs passées sont bien les bonnes, sans pour autant ajouter des tests dynamiques ou des annotations explicites partout.

Attention, si tu veux faire du code facilement "maintenable" portable et "refactorisable", les contrats sont indispensables.
De plus ils te permettent de définir le responsable dans l'erreur d'un programme. Les contrats ne sont pas forcément aussi simples qu'on peut le penser. Exemple pour l'échantillonnage d'un signal, il peut être utile de mettre le théorème de shanone comme condition d'entrée. Idem pour les invariants etc.
Enfin peut être qu'on ne parle pas de la même chose.