Maths with Coq in L1, a pedagogical experiment

TL;DR

This paper discusses a three-year pedagogical experiment teaching formal proofs with Coq to first-year university students in France, highlighting practical sessions, methodology, challenges, and potential improvements.

Contribution

It introduces a hands-on Coq-based introductory course for L1 students, detailing its development, methodology, and pedagogical insights over three years.

Findings

Students gained practical experience in formal proofs.

The course evolved to address technical and pedagogical challenges.

Room for improvement identified in teaching methods and materials.

Abstract

In France, the first year of study at university is usually abbreviated L1 (for premiere annee de Licence). At Sorbonne Paris Nord University, we have been teaching an 18 hour introductory course in formal proofs to L1 students for 3 years. These students are in a double major mathematics and computer science curriculum. The course is mandatory and consists only of hands-on sessions with the Coq proof assistant. We present some of the practical sessions worksheets, the methodology we used to write them and some of the pitfalls we encountered. Finally we discuss how this course evolved over the years and will see that there is room for improvement in many different technical and pedagogical aspects.