Valentin Bergeron
Engineering Manager & Tech Lead
À propos de Valentin
Passionné par la programmation fonctionnelle et la vérification formelle, Valentin aime relier la rigueur des assistants de preuve et le pragmatisme du code de production.
Ingénieur backend depuis une dizaine d’années, il explore sur son temps libre comment faire entrer les preuves formelles dans le code de tous les jours, notamment grâce à l’IA.
Son talk
Solide comme un Rocq : une introduction au vericoding
Les tests et les types sont censés nous protéger des bugs. Mais qui vérifie que ces garanties tiennent vraiment ?
Aujourd’hui, les agents IA écrivent du code plus vite qu’on ne peut le relire. Cette question n’a jamais été aussi urgente.
Le vericoding, c’est l’idée de faire de la vérification formelle un outil du quotidien : sortir les assistants de preuve comme Rocq des labos de recherche pour les mettre entre les mains des équipes qui livrent en prod.
Écrire une preuve, c’est dur. Écrire ce qu’on veut prouver, beaucoup moins. C’est là que l’IA entre en jeu : vous dites ce qui doit être vrai, la machine se débrouille pour démontrer pourquoi. On obtient alors des garanties d’un nouveau genre : des interfaces qui ne sont plus des promesses, mais des contrats prouvés.
On commencera par repérer le code qui mérite d’être prouvé : les invariants, les machines à états, les règles métier où un bug ne se résume pas à un incident mais peut coûter très cher. On verra où la preuve rapporte gros, et où elle ne vaut pas l’effort.
Ensuite, on passera à la pratique : comment livrer du code prouvé. Backend, frontend, systèmes événementiels, jusqu’au firmware embarqué, on verra comment déployer ce code et ce que ça change dans votre archi et votre codebase quand vous savez que ça marche.
On a commencé par douter de nos garanties. On repartira avec des fondations solides comme un Rocq.