Comment by bvrmn

TLA+ has its own quirks, you could add sugar here and there, but from semantic standpoint you couldn't do much. It's "unreadable" because requires some mental model most of developers don't have. My point: you either provide "simple" tools which could do nothing for real models or they become on same level of "unreadableness" really fast.