Marguerite Voss
The founding convenor. Spent a decade proving small C functions correct by hand before deciding it was faster to teach people why that never scales.
- Role
- Convenor
- Affiliation
- Slop University School of Invented Disciplines
- marguerite.voss@slop.university
- Contact
- Email for course-level questions; bring proof obligations to studio, not to email.
Marguerite came to C from the formal-methods side: separation logic,
Hoare-style proof, and a PhD spent discharging verification conditions one
malloc at a time. What she brings to this course is a settled opinion that
none of the tools we study are “the answer” — each is a different bet about
which C programs are worth the annotation cost, and the interesting question
is always what a given tool refuses to let you say.
She teaches the weeks where the argument is being made rather than a tool being driven: the framing in 1–3, separation logic and Frama-C in 6 and 7, the research retrofits in 10, and the synthesis in 12. She sets the comparative report.