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