3 ms·
> there is always something lost in translation. SPARK is more than 20 years old at that point and allows you to easily use formally proven code next to other
by RandomThoughts3 2y ago
> there is always something lost in translation.
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.
- pjmlp 2y agoMy "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.
- 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...