Merci pour cette belle introduction à un sujet passionnément abstrait.
Le titre parle d'assistant de preuve mais focalise surtout sur les preuves de programmes je comprends que c'est bien naturel sur ce site... Néanmoins avec Isabelle on glisse un peu vers la preuve purement 'mathématique' et le domaine inclut d'autres logiciels comme Mizar et Metamath qui me fascine depuis près de 30 ans de part sa simplicité théorique basée uniquement sur des substitutions.
Les preuves de programmes ne sont pas toujours aussi fastidieuses mais le volume des démonstrations contribue dans les deux cas à dissuader leur usage. J'attends toujours l'automatisation qui rendra tous ces outils plus accessibles.
# 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é à 2.
Merci pour cette belle introduction à un sujet passionnément abstrait.
Le titre parle d'assistant de preuve mais focalise surtout sur les preuves de programmes je comprends que c'est bien naturel sur ce site... Néanmoins avec Isabelle on glisse un peu vers la preuve purement 'mathématique' et le domaine inclut d'autres logiciels comme Mizar et Metamath qui me fascine depuis près de 30 ans de part sa simplicité théorique basée uniquement sur des substitutions.
Metamath est la version informatique du livre illisible Principia Mathematica et permet d'admirer une preuve formelle de 2+2=4
Les preuves de programmes ne sont pas toujours aussi fastidieuses mais le volume des démonstrations contribue dans les deux cas à dissuader leur usage. J'attends toujours l'automatisation qui rendra tous ces outils plus accessibles.