I liked the article and tried to look into TLA+, but the documentation is off-putting at every turn. There is no HTML documentation, you need to download a ZIP of a book. Opening the ZIP, it's not just a single PDF, it's a bunch of PDFs (many a page or paragraph long) that the table of contents hyperlinks to. This makes impossible to skim the documentation.

Looking at some examples, it looks like TLA+ uses non-ASCII symbols which are then maybe mapped to ASCII? As such, you need to remember lots of obscure sigils, and I couldn't find a high-level intro of how it works.

It sounds very interesting, but the documentation could be made much more helpful. Lamport comments that "people nowadays don't read, so I made a video course", but I'm not surprised people don't read if reading is this hard. (I personally dislike video courses because you can't skim them and would much prefer HTML documentation).