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

Peut-on changer le monde ? Programmation impérative, effets monadiques, effets algébriques