Skimming through it, some thoughts.
The one thing that I want to dig into more is that he says that he doesn’t think it will be useful for programmers, besides changing how you think about systems in a good way. I vehemently disagree: TLA+ is incredibly and directly applicable to programming. I love advocating it not because I think the ideas are brilliant (they are, Lamport’s a genius), but because it Makes Your Software Better.
Why not embed Youtubes?
I guess he wanted the ability to show the website at certain points. For the initial video, he only used it to provide links, which can be done with Youtube as well. Maybe there will be more exciting things in later videos? For example, interactive examples.
I would watch this just for his sense of humor.
Okay actually the costumes are the highlight.