PlusCal is not higher level, it just has constructs that programmers are used to, like assignment, sequential composition, processes and procedures. Even in thi

PlusCal is not higher level, it just has constructs that programmers are used to, like assignment, sequential composition, processes and procedures. Even in this particular case the specification would be clearer in TLA+ than in the PlusCal version, had it not been a translation of the latter. For example, the PlusCal version contains an unnecessary and confusing sequential composition of the send and receive bits.