With the rise of MOOCs, much attention has been paid to how programming language technology can help facilitate programming education. This has taken many forms, for example, automatic grading, generation of problems and feedback, and program execution visualization. However, for all of its close connections with programming, mathematical proof has not enjoyed the same level of automation and support. Students still write proofs by hand, and those proofs are hand-checked by a teacher and their TAs, a situation that clearly does not scale. Could we use programming language technology to help facilitate pedagogy around mathematical proof like we do with programming?

To explore this question, we are developing an online tutorial for mathematical proof by induction through functional programming called InductFun. Students develop functional programs in a restricted functional programming language and then prove properties about them directly in InductFun. The platform is backed by the Coq proof assistant.

In this talk, I present the current state of InductFun and discuss our on-going work in creating a tool that supports pedagogy around proofs. In particular, I discuss the design space surrounding InductFun where we balance the strength of a proof assistant with the needs of educators teaching proof in computer science courses.