Une interface pour faire des maths
avec Loïc
Loïc est chargé de recherches à l'Inria-Sophia.
Sur ma demande, il a entrepris depuis deux ans de développer
une nouvelle interface, Coqweb,
pour faire des mathématiques sur ordinateur.
Il est évidemment à l'écoute de mes
suggestions, et
nous en discutons une après-midi par semaine.
Le challenge consiste à trouver le compromis convaincant entre
deux
façons de faire des maths qui sont à première vue
radicalement différentes:
la pratique traditionnelle des enseignants et des chercheurs,
et la pratique des utilisateurs de notre assistant de preuves favori, Coq.
Cette interface, en constante évolution, est déjà suffisamment conviviale
pour être
utilisée depuis un an par deux cents
étudiants de première année à Nice (via WIMS).
Nous discutons aussi depuis des mois une nouvelle version
qui sera
adaptée aux besoins des chercheurs (et non plus des étudiants).
L'interface sera bientôt accessible par le web.
En attendant, si
ça vous interesse, n'hésitez pas à nous mettre un mail.
André Hirschowitz
Last
modified: December2005