Scaffolding TLA+
I’m in the process of updating my TLA+ workshop for my class next week.1 Every time I run it I get new ideas on what to improve. After April’s class, one of the most important changes I noticed was also one of the smallest. In TLA+, there’s two ways to write “not-equals”: # and /=. I’m used to writing /= and find # really weird, so I teach /=. After April, I mass changed every /= to #.
Most people approach formal methods like they’re learning a new programming language. This is understandable, but also a mistake. Specifications serve a different role and have to be thought about differently than implementation details. When teaching TLA+, I’m simultaneously covering three topics:
The only way to really build a mental model is through regular practice and feedback. You try things out, make mistakes, and learn from them. This is necessary but also slow and painful, so much of teaching is finding ways to speed this up. Creating specific controlled environments where mistakes are obvious and the feedback is both quick and comprehensive. Anything that slows this down is something I want out. One of the biggest impedances is overload: if you’re faced with three new concepts at once, you can’t easily get feedback on just one of them. You have no idea where your mistakes are and which things you are misunderstanding. It takes less time to learn five things sequentially than three things simultaneously. The practice of designing the learning environment so students only have to learn one idea at a time is called scaffolding.
TLA+ is notoriously hard to learn. This is mostly attributed to the concept of specifying, but a huge part of the problem is how hard it is to scaffold TLA+. This is because topic (3), TLA+’s syntax, so unfriendly for beginners. Much of it is intuitive to experienced practitioners but gets in the way of initial learning. Students spend so much time wrestling with the syntax that could be better spent on the core concepts.
