>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.
Bold statement, at least in that case you know the algorithm isn't wrong.
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.
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...