This paper lays out a case study of Software Construction, a new course in the undergraduate computer and communication sciences curriculum at EPFL. We hope to share some generalizable lessons we learned from running its first edition in Fall 2023. The course targets three core concepts—functional programming, real-world engineering, and correctness—and its design is informed by four principles—students should learn by doing, assignments should be self-motivating, knowledge should be built incrementally, and students should see progress over time. We illustrate how we realized these concepts and principles with practical examples of course materials and teaching methods that we hope will serve as useful inspiration to others teaching similar courses. Lastly, we present some encouraging preliminary data about course outcomes and share our speculations about experiments for its future evolution.

tl;dr: String diagrams are an intuitive diagrammatic representation of some pretty useful math. This being Interactive Theorem Proving, of course, I want to formalize that math in a proof assistant (Coq), in such a way that formal proofs still work like paper proofs using all the nifty properties of the diagrammatic representation. And, of course, a naïve formalization runs into problems that make the system painful to use. So this project explores how we might overcome those problems and restore the convenience of string diagrams in a formal setting.