Teaching Unifying Theories of Programming
摘要
Teaching Unifying Theories of Programming (UTP) exposes a recurring problem in formal methods education: realistic semantic models are rich, but students learn only when they can see a clear next step. Our central claim is that UTP is most effectively taught not primarily as a semantic meta-theory, but as a disciplined method for specifying, calculating, and refining programs. In this FMTea keynote paper, we argue that we should organise UTP teaching around three linked unifications: across theory families, across abstraction levels, and across semantic presentations. With this organisation, we give students a stable route through the subject. They learn one core relational and refinement calculus, then reuse it across designs, reactive contracts, linked models, and beyond. They connect requirements to implementations through explicit refinement steps, and they view denotational, operational, and algebraic accounts not as competing definitions but as mutually justifying views of the same theory. The paper presents a course architecture centred on a minimal teachable core, and a taxonomy of exercises to develop refinement literacy in contracts, refinement, reactivity, and semantic linking. Drawing on experience from university courses, intensive schools, regional programmes, and industrial delivery, we argue that the most effective way to teach UTP is to make procedures explicit, make side conditions visible, and provide fast feedback. We conclude by outlining a lightweight tooling and artefact agenda that supports research-led teaching without imposing the full cost of mechanisation.