[superidiot1932]

>It is meaningless to model a great algorithm in abstract mathematical models, and then let someone else implementing them in C89 with raw BSD sockets and C strings

Bold statement, at least in that case you know the algorithm isn't wrong.

[pjmlp]

Which is worthless without the guarantee that the C code actually implements the algorithm as designed.

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.

[polyglotfacto2]

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...