When I did spend a little amount of time trying to learn TLA+, the biggest annoyance is the two different syntax/form in which TLA+ can be written, a mathematical symbolic form, and a text form like a program.

Now, this topic is a rather abstract and difficult to comprehend one, and having two equivalent ways of doing it, introduced right from the beginning, I thought was too much of a cognitive load, considering the difficulty of the subject.

I hope this material from the article is simpler for learners.