I have the same opinion about the beauty of TLA+ vs PlusCal, so I find PlusCal frustrating to read. But I don't think the original poster was giving a dismissi

I have the same opinion about the beauty of TLA+ vs PlusCal, so I find PlusCal frustrating to read. But I don't think the original poster was giving a dismissive opinion of PlusCal. Lamport's genius here is that he made TLA+ accessible via PlusCal. I appreciate this, as well as the video lectures which he made because he "realized that people don't read anymore...".