Easy and fun introduction to TLA+ for children?

[dmah...@gmail.com]

So, having just read this article on The Atlantic "The Coming Software Apocalypse"..

https://www.theatlantic.com/technology/archive/2017/09/saving-the-world-from-code/540393/

..I must ask, is there some way to make this accessible for children and young adults? I don't seem to be finding anything doing a Google search for "TLA+ for kids".

Do you have to be an utter genius to understand this, with years of formal training at a college/university? Or is there some way to make it easy for youngsters to get a glimpse of it?



I would suggest taking a look at Scratch, a visual block assembly system for teaching programming to children, that doesn't require typing any code to make functional programs. Just drag blocks around and snap them together.

https://scratch.mit.edu/

(Scratch based on Flash which we all know is dying out, but there's a fork of it called Snap! that is pure Javascript / HTML5, requires nothing to be installed to use it, and can save to cloud storage.)

http://snap.berkeley.edu/



Of course, you can't do anything significantly complex or important with Scratch/Snap!, like write a vehicle automation system, or a 911 call routing system, but that's not the point.

Getting kids to think logically about how to problem solve, is the point. If it's fun and draws them in, and gets them interested in assembling code blocks and making shapes fly around the screen and make noises without having to know anything about syntax, order of operations, APIs, CLIs, file paths, text editors, etc, that is the point.



So, would there be some way to implement the essence of TLA+ as a GUI browser / tablet implementation, with draggable tiles and shapes, a touch interface, etc, and make it very easy for youngsters to grasp, without drowning them in complex technical abstractions?

If you want a revolution, then I think you are going to have to start as young as possible, and possibly before a potential new user of this "better way" of designing software has even seen regular typed programming.

[Leslie Lamport]

A good analogy to teaching children TLA+ would be teaching them
group theory.  The mathematical prerequisites for group theory are
trivial--knowledge of what a set is will suffice.  And I'm sure you
can teach group theory to children.  But it would be a disaster
because it would be impossible to motivate the children.  There's
nothing to make them want to learn group theory.  They can't create
games or pictures with it.

The prerequisites for using TLA+ are also elementary.  They should
probably be taught in high school, but should certainly be taught in
the first year of a computer science or math education: sets,
functions, and elementary logic.  Unfortunately, the teaching of this
elementary math is terrible, and even most computer science students
wind up being frightened of math and with no idea of how it could be
useful in building computer systems.  Fortunately, if they can
overcome their fear, using TLA+ will teach that math to them.

The kinds of errors that the Atlantic article started by talking about
aren't going to be eliminated by the kinds of visual tools it then
talked about.  They can be eliminated only by properly thinking about
what the program is supposed to do and how it should do it.  And,
unfortunately, most people would rather code than think.

If you want a revolution that will change the situation, you need to
teach kids that math is fun and easy.  TLA+ can teach that to motivaed
engineers, I don't think it can teach it to kids.

Leslie

[a...@anm.me]

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

[Leslie Lamport]

I'm still skeptical, but I'd love to be proved wrong.  If you're in the S.F. Bay Area, please contact me privately and let's see if we can get together to discuss this.

Leslie

[Ron Pressler]

You can certainly teach first-order logic and basic set theory to kids (highschoolers, I guess). This teaches both mathematical thinking and formalization. While it is not its primary goal, I think TLA+ (and TLC) is a _great_ way to play with FOL/ZFC. I'm sure a more basic UI can be built for TLC just for loading files and evaluating expressions.

Ron