Je ne prétends pas débattre avec le niveau requis, mais peut on encore parler de démonstration quand c'est "trivial" et que cela tient en une ligne ?
De ce que je comprends il y a une sorte de consensus qui considère que les preuves formelles n'ont pas besoin d'aller au delà d'un certain niveau de détail. Les résultats "triviaux" n'ont pas à être démontrés et peuvent simplement être placés dans une bibliothèque. Intellectuellement ça me déçoit et en pratique cela introduit un risque de bug proportionnel à la taille de la "bibliothèque".
[^] # Re: Preuves de programme et preuves de théorèmes
Posté par chansen . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 1.
Je ne prétends pas débattre avec le niveau requis, mais peut on encore parler de démonstration quand c'est "trivial" et que cela tient en une ligne ?
De ce que je comprends il y a une sorte de consensus qui considère que les preuves formelles n'ont pas besoin d'aller au delà d'un certain niveau de détail. Les résultats "triviaux" n'ont pas à être démontrés et peuvent simplement être placés dans une bibliothèque. Intellectuellement ça me déçoit et en pratique cela introduit un risque de bug proportionnel à la taille de la "bibliothèque".