SPARK is more than 20 years old at that point and allows you to easily use formally proven code next to other ADA code. Sorry but implying that the issue is things “lost in translation” is a complete cope out.
I’m very sour about the disdain for formal proof in the field. I understand the wish to iterate fast for user-facing elements but the fact that we use the same development techniques for the backbone of our infrastructure is nothing short of insane from my point of view.
There is a self defeating attitude with regard to formal tool which is that they are too costly and too complicated to use outside of things for which they are mandatory. It means people are not trained in how to use them so it’s hard and costly to find someone who will prove your code and this vicious cycle somehow feeds itself.
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.
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...