Dans les faits, la cohérence interne que tu peux vérifier est assez faible. Comme les gens détestent écrire les choses 2 fois, tu te retrouves à faire des calculs avec des données que tu as déjà, plutôt que vérifier que 2 valeurs sont cohérentes.
Pour l'exemple que tu donnes, cela tombe exactement dans ingénierie des modèles et le genre de petites règles que tu peux écrire. C'est très utile, tu peux augmenter très largement la productivité des utilisateurs. Mais tu ne vérifies pas de cohérence en soi, tu écris la règle elle-même. On est très loin d'une "vérification formelle".
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Dans les faits, la cohérence interne que tu peux vérifier est assez faible. Comme les gens détestent écrire les choses 2 fois, tu te retrouves à faire des calculs avec des données que tu as déjà, plutôt que vérifier que 2 valeurs sont cohérentes.
Pour l'exemple que tu donnes, cela tombe exactement dans ingénierie des modèles et le genre de petites règles que tu peux écrire. C'est très utile, tu peux augmenter très largement la productivité des utilisateurs. Mais tu ne vérifies pas de cohérence en soi, tu écris la règle elle-même. On est très loin d'une "vérification formelle".
"La première sécurité est la liberté"