Forge: A Tool and Language for Teaching Formal Methods
summary
Forge is a reworked Alloy designed to teach formal methods incrementally: it implements language levels (froglet → relational → LTL) that restrict expressive power and give pedagogical error messages, adds custom visualization via small JavaScript renderers, and introduces testing constructs to bridge unit tests and models. The tool uses Alloy’s solver backend, ships artifacts, and undergoes multi-year classroom evaluation with over a thousand students; students successfully build diverse projects, though long traces and JS visualizers remain practical limits.
AI-written summary · about
chapters (12)
- 0:00Formal methods for students
- 1:04Alloy demo: modeling & verification
- 3:55Alloy shortcomings for education
- 5:23Introducing Forge
- 6:03Forge language levels
- 10:00Custom Forge visualizations
- 12:53Forge student project evaluation
- 13:55Forge availability & future
- 14:36Q&A: visualizations & scaling
- 16:24Q&A: problem size & solver limits
- 17:27Q&A: student authenticity
- 18:31Q&A: gradual verification