13 ms·
>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 str
by superidiot1932 2y ago
>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 2y agoWhich 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 2y agoYou 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-for-concurrent-programming-365d9eeb491e https://medium.com/@polyglot_factotum/why-tla-is-important-f...