> I would love to see somebody who thinks deeply about PL syntax to make another language with the same semantics as TLA+

Perhaps you would find Quint interesting? https://news.ycombinator.com/item?id=41111790

There's a comment that says Quint uses TLA+ as its base language: https://news.ycombinator.com/item?id=41118162

Disclaimer: I don't know anything about TLA+ or Quint, I just remembered seeing Quint here