A Teaching Language for Specification

on YouTube ↗30m

" summary

A compact teaching language called LSL (Logical Student Language) builds on ISL so students spend little time on syntax and much time on real specification work. It uses contracts + generators for runtime checking and property‑based testing, adds lightweight verification via Rosette symbolic execution to find deep bugs that random tests miss, and scales to assignments like a simple memory allocator and a distributed snapshot algorithm. Course materials and the Racket package are public and a two‑week Lean bridge shows full proofs.

AI-written summary · about

" chapters (13)

1. 0:00Teaching language for specification
2. 1:04Teaching formal specification
3. 3:11Proof assistants in courses
4. 6:19Logical Specification Language
5. 7:25Informal to formal specs
6. 9:52Property-based testing with contracts
7. 11:37Lightweight verification
8. 13:03Transitioning to Lean
9. 14:05Advantages of teaching language
10. 16:36Course structure with design recipes
11. 19:47Live demo: contracts & testing
12. 24:47Future improvements & materials
13. 26:45Q&A