You are right that it would be great if the code was generated automatically, but wrong that there is no value in using TLA otherwise.
When you are writing code, do you have an idea in your mind of what you are trying to implement? TLA is not for checking the code, it is for checking that idea. I explain this in more details in another article: https://medium.com/@polyglot_factotum/why-tla-is-important-f...
Something that manual translation cannot provide.
If the algorithm was validated in F*, and having the C code generated, great.
Now doing it in TLA+, and then implementing it as copying from a algorithms and datastructures book with Pascal like pseudo-code, not so great.