Teaching Logic and Set Theory with Dafny
summary
Course materials use Dafny as a teaching assistant and programming language plus proof assistant to give instant feedback on assignments and to speed grading without fully automating it. Exercises include set algebra (right distributivity, set difference non‑associative with an explicit witness), cardinal equivalence and Cantor diagonalization in four lines using infinite set comprehension, and a formalized natural‑deduction DSL where proofs are data. One class moment: students compress a 31‑line paper proof into a 14‑line verified Dafny proof; class size runs about 30–70.
AI-written summary · about