Ça me fait penser à un truc que je n'ai pas cité dans la dépêche, mais qui est un phénomène bien connu chez les utilisateurs d'assistants de preuve.
Il est clair que prouver formellement est difficile, mais ça a un côté jeu vidéo très addictif. En particulier, je connais pas mal de gens qui sont capable de passer des heures sur Coq afin de venir à bout d'un théorème. Il semble clair que cela est provoqué par l'interactivité des prouveurs, qui ont un air certain de point-n'-click. Je connais même des gens qui se font réprimander pour avoir passé trop de temps sur Coq...
Bref, les preuves formelles, contrairement à ce qu'on pourrait croire, c'est marrant. Et à coup sûr plus fascinant que Flappy Bird.
[^] # Re: Idris
Posté par Perthmâd . En réponse à la dépêche Sortie de Coq 8.5 bêta, un assistant de preuve formelle. Évalué à 10.
Ça me fait penser à un truc que je n'ai pas cité dans la dépêche, mais qui est un phénomène bien connu chez les utilisateurs d'assistants de preuve.
Il est clair que prouver formellement est difficile, mais ça a un côté jeu vidéo très addictif. En particulier, je connais pas mal de gens qui sont capable de passer des heures sur Coq afin de venir à bout d'un théorème. Il semble clair que cela est provoqué par l'interactivité des prouveurs, qui ont un air certain de point-n'-click. Je connais même des gens qui se font réprimander pour avoir passé trop de temps sur Coq...
Bref, les preuves formelles, contrairement à ce qu'on pourrait croire, c'est marrant. Et à coup sûr plus fascinant que Flappy Bird.