We will present our early experiences teaching first- and second-year computer science students in Coq, adapting Logical Foundations (the first volume of Software Foundations). Our presentation’s goals are: to offer evidence that such a course is pedagogically sound; to highlight the pedagogical approach taken to teaching Coq and informal proof simultaneously; to document successes and failures, both pedagogically and in Coq’s technical ecosystem; and to seek feedback on pedagogy and course design.

The first author will give the talk.