[mon avis] Lean-lang (lean4) vaut le détour, c’est un langage de programmation sympa (fluide, concis, élégant, puissant, etc.), mais surtout, c’est un environnement qui permet de prouver ses programmes.
Je ne dirais pas qu’il est simple (en particulier pour les preuves), mais c’est très encourageant pour l’avenir.
S’il me semble délicat de l’utiliser avec des étudiants juste pour quelques séances (je crains qu’il ne faille lui consacrer plus de temps), on peut au moins le leur montrer.
Pour se faire une idée, j’ai fait quelques vidéos :
- intégration de lean dans Jupyter (on peut donc, raconter, programmer, exécuter, tester et prouver en jupyter)
- premiers programmes et programmes suivants (quand les problèmes arrivent)
- premières preuves
J’espère que Lean va progresser encore et devenir vraiment facile à utiliser pour tout le monde (novice et expert) et sur tous les sujets (programmation et preuve).