Learn 'em Dafny
summary
A programming‑first software correctness course uses Dafny with a flipped classroom and automated, proof‑based feedback for about 120 required students, showing measurably better course evaluations. Concrete points: Dafny verifies methods by contract but functions by implementation, expression versus statement syntax forces confusing refactors (semicolon, var versus const/ghost), module‑level mutability rules trip students, and version 4.0’s ghost fixes reduce some friction. The talk gives specific classroom practices and precise language changes that shorten the learning curve.
AI-written summary · about
chapters (11)
- 0:00Teaching with Dafny
- 1:26Course design challenges
- 3:33Programming-first approach
- 5:38Flipped classroom benefits
- 7:28Design by contract
- 8:52Methods vs functions
- 10:15Syntax and semantics
- 12:42States, predicates, monads
- 14:50Semicolons confusion
- 16:59Dafny 4.0 improvements
- 18:01Conceptual models
related talks
15mOn the Impact of Formal Verification on Software Development
24mPassing Down the Pain: Difficulties in Teaching Software Development
01h 01mDeclarative Programming and Education
01h 54mPair Programming & Test Driven Development done right
33mThe Art of Teaching
39mClean, Concise, Collaborative Code
34mThose Who Can Do Should Also Teach
01h 04mIn Defense of "Little Code"