People get confused when language implementations break language guarantees
16 hours ago
- Imperative languages like Python execute assignments sequentially in temporal steps, while TLA+ separates updates from temporal steps, making order irrelevant in its semantics.
- TLA+ beginners encounter issues when using undefined variables (e.g., y' before assignment) because verifiers like TLC require a specific order for assignments, breaking the nonordering guarantee.
- Side-effecting operators like PrintT, Assert, and IOExec in TLC violate TLA+'s side-effect-free semantics, causing unintended effects like ghost prints when guards fail.
- There is no visual distinction between safe TLA+ operators and TLC's escape hatches, leading to confusion, similar to Prolog's cut or other declarative languages' exposed operational features.
- The text draws parallels to Neel Krishnaswami's observation that least-loved features in declarative languages are those that break declarative semantics by exposing operational details.