Teaching Software Specification (Experience Report)
summary
Course redesign puts software specification front and center for first-year students and builds a tiny custom language that adds contracts and property-based testing plus a lightweight concurrency model so assignments actually include a timing side‑channel fix, a compiler optimization proof, multiple maze representation roundtrips, a simple memory allocator, and a working Lamport snapshot implementation. Runtime contract checks and generated test inputs find counterexamples quickly, student interviews report better transfer to real tools, and course artifacts and code are available for reuse.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:27Teach specification early
- 3:54Student feedback
- 5:40Five lessons learned
- 7:02Freshman assignments
- 9:32Building specification confidence
- 10:37Contracts and property testing
- 13:28Pedagogic language design
- 15:56Skill transfer to real languages
- 17:20Student perspectives
- 18:46Key course changes
- 20:34Q&A
related talks
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
22mThe New Code
23mStop Making LLMs Deterministic: A Spec-Driven Software Factory
01h 02mBasics Designs and How We Got Them Wrong
32mDesign of Software Representation Languages: a Historical Perspective
50mSoftware Is Details
01h 07mThere Is Only One Time in Software (Language) Engineering!
28mWhat You See Is What It Does: A Structural Pattern for Legible Software