If a TLA+ transpiler could emit Python, Javascript, Java, C, Rust, C++, Go (even just one of these), it would be infinitely more usable in that it helps you cro

If a TLA+ transpiler could emit Python, Javascript, Java, C, Rust, C++, Go (even just one of these), it would be infinitely more usable in that it helps you cross the gap from "I know my TLA+ is correct" to "I know my Go is correct". Or as a baby step, does TLA+ emit comprehensive test cases? Then we as programmers still have to do the hand transpilation step, but at least we can be assured our implementation is correct (if not efficient).