I understand, but I think this strikes at the core of our pedagogical differences regarding TLA+ -- after all, TLA+ is super-Turing-complete, and even TLC can check a subset of TLA+ that is still effectively Turing-completish. Of course you can specify at any level in TLA+, and people have even written compilers from C and Java to TLA+. But doing so suffers from the same scalability problems that all code-level verification techniques suffer from.
The question we're asking is how best to get people to use TLA+. Do you show them what model-checking can do and then show that TLA+ can model virtually anything and TLC can check many things, and do so at the code-level because that is something they already know from programming -- but then they ask, as they do in this discussion, why you need TLA+ at all if all you're doing is translating Go to some other language -- or do you first try to show them the TLA+'s real strength, which is mathematical modelling of systems, but that is a new concept that is different from programming and can be foreign to them?
It's a hard problem, and maybe the right approach is to do both, which is what you're doing if we take this post together with others you've written. But I think it's worth mentioning that in this case, this is not the spec someone who knows both TLA+ and Go well would likely write.
BTW, I'm trying to remember which of those two features sold me on TLA+, and I think it was the combination of both. I knew the limitations of model-checkers (and had worked with NASA's Java model-checker before) that I knew that a model-checker alone wouldn't give me what I need for the complex distributed system I was working on, and mathematical modelling alone of something so subtle wouldn't have sufficed either without some help checking (cheaply!) if my ideas were right or wrong. So neither aspect would have sold me in isolation, I think.