Mathematics is the foundation of computer science and a core portion of a computer science undergraduate’s curriculum. Formal reasoning, in particular, is essential for rigorous algorithmic design. However, undergraduates often fail to appreciate the value of mathematical proof in their studies, likening proof to a purely academic exercise with little application to real-world programming. Furthermore, students also fail to grasp the mechanics of mathematical proof, which makes subsequent learning unfocused and frustrating. This problem could be addressed with consistent feedback, but generating useful feedback for student work is a time-consuming process for the instructor that does not scale well with large class sizes. As a result, students receive too little feedback too late on their work to make learning efficient or even possible.

I believe that the programming languages community has a unique set of perspectives and tools to offer the computer science education to alleviate these concerns. However, applying these perspectives and tools requires that we, as programming language researchers, are sensitive to the specific pedagogical demands of instructors and the behaviors of students. In this lightning talk, I outline steps that the programming languages community can take to address these shortcomings in mathematics education in computer science and introduce the work that my collaborators and I have done to bridge this gap.