Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Qu'est-ce que l'égalité ? De Leibniz à la théorie homotopique des types