Re: Easy and fun introduction to TLA+ for children?

[a...@xxxxxx]

Hey there,

I'm Andrew from the Blockly[1] team at Google.  We're also working with the Scratch team on scratch-blocks[2].

We think this is a great idea, and could be used to introduce test-driven development, encouraging a focus on edge cases instead of nominative cases.


In particular, Blockly's focus is on generating text code from Blocks, and we support adding new languages.  For TLA+, you'd have you write a new generator from scratch, and probably a new library of Blocks. I'm not sure many of our predefined blocks (designed for procedural programming) would be useful.

Using blocks means kids don't have to worry quite as much about the syntax, and rely more on recognition (a toolbox full of visual blocks) than recall. And the generation of code makes it easier to transition kids to more traditional programming.


As for making it fun, I'd love to see if TLA+ could support programming agents/non-player characters in a game world. That could probably lead to enough variety in world state (including changes over time) to force interesting decisions.

Doing such complicated worlds in Scratch can often be tedious and fragile, and TLA+ (from what little I've explored) looks like the perfect counterpoint to should better practice.

If anyone wants to explore the Blockly side of things, please reach out to us at the Blockly forum[3].



1: https://developers.google.com/blockly/
2: https://github.com/LLK/scratch-blocks
3: https://groups.google.com/forum/#!forum/blockly