My "lost in translation" remark naturally doesn't apply to SPARK, rather to stuff like TLA+ that don't have any mapping to actual programming languages, unlike stuff like Ada/Spark, Frama-C or even Design by Contract.
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, without any relation between the mathematical model and the C implementation.
>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.
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...
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, without any relation between the mathematical model and the C implementation.