> If it takes a programmer in a specific (unused) programming language to write a specification TLA+ isn't a programming language, it's a specification languag

> If it takes a programmer in a specific (unused) programming language to write a specification TLA+ isn't a programming language, it's a specification language. Programming languages are much too concrete to evaluate designs; that's why specification languages (like TLA+) exist. You "test" a TLA+ design by running a model checker (usually TLC) that verifies the design meets the spec (i.e. a bunch of invariants which are the TLA+-equivalent of unit tests).