Collaborative Research: FMitF: Track III: Integrating Formal Methods into the Foundational Undergraduate Curriculum

Mathematics and computer science are inextricably linked. However, it is well-known among educators and education researchers that undergraduate computer scientists often do not appreciate the relevance of mathematics to their discipline. This disconnect adversely affects students, especially as they progress from concrete, practical introductory courses centered on programming to theoretical upper-level courses rooted in abstract mathematics. Researchers have observed that student performance in the classroom and retention within the major falter when these connections are not established. This project's impact is to address these concerns by developing pedagogy that (a) unites the mathematical foundations and practice of computer science together in a way that all undergraduates can appreciate and directly apply in their future endeavors and (b) is adoptable by as many institutions as possible, especially those with limited room to expand their curriculum. To accomplish these goals, the investigators develop, deploy, and evaluate new pedagogy that integrates formal methods techniques within the existing undergraduate computer science curriculum. Specifically, this pedagogy introduces program reasoning, an activity all computer scientists perform, as the primary vehicle for studying the mathematical foundations of computing in the contexts of introductory programming, discrete mathematics, and algorithms courses. Such pedagogy bridges the gap between mathematics and computer science for all undergraduate computer scientists and makes relevant formal methods for a new generation of programmers. Additionally, the project promotes the relevance of formal methods to undergraduate computer science educators, as exemplified by this pedagogy, through a series of workshops at the regional and national levels. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.