Lamport, Dijkstra, Scholten, Hoare, and Knuth, to name just a few, are giants in the field who routinely read each other’s work. I’m positive TLA+ is directly i

Lamport, Dijkstra, Scholten, Hoare, and Knuth, to name just a few, are giants in the field who routinely read each other’s work. I’m positive TLA+ is directly influenced by predicate transformer program semantics.