TLA is one of the systems that are actually very practical. You can go up or down as many abstraction layers as you need . There's a great introduction written by @pron on his blog [1].
However, it's worth pointing out that you don't magically get the final program out of the TLA proof. The proof only works for the abstraction level that you chose to write it at.
However, it's worth pointing out that you don't magically get the final program out of the TLA proof. The proof only works for the abstraction level that you chose to write it at.
[1] https://pron.github.io/