Diagrams are rare and hard to work with in programming and theorem-proving environments. Existing diagramming systems do not meet the practical needs of interactive, exploratory use, such as keeping diagrams understandable as they grow in size with limited screen space, or as they evolve as the user steps through the program or proof. My research seeks to develop an approach—compositional diagramming—that meets these needs. Diagrams are formed of independent parts composed in systematic ways reflecting the structure of the represented object, and the diagramming system compiles a higher-level description of the object to lower-level diagram components. Techniques that make diagrams more practical, such as wrapping, folding, and packing, fit neatly into a compositional approach. Through my work, I hope to build a useful diagramming system for working computer scientists, mathematicians, and programmers, based on a better understanding of compositional diagrams.

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.