[marco_salvatori]

Doing the comparison TLA vs Rust as programming languages is a misunderstanding. It's exactly equivalent to the misunderstanding in a comparison like "what's the advantage of SQL over Rust, that as far as I know is designed specifically for this kind of problems". Now, one could believe, perhaps, that Rust is "designed specifically" for the implementation of database "kind of problems". But the conclusion that there is therefore no "overwhelming advantage" to databases would not follow from that belief.

TLA and the TLA tools form a model checker. The TLA language is not used to do computations,but, rather, is used to describe properties and behavior of complex systems. The TLA tools then machine validate the descriptions to assure that the evolution of a system with the given behaviors will satisfy expected correctness properties. A TLA specification tells you that if your system is implemented (in a computer language, like say Rust) according to the description then the systems operation will satisfy the validated correctness properties.

TLA is about answering the question "Do I properly understand my problem and will my solution logic satisfy problem needs?". Rust doesn't help answer that question.