3 ms·

> Someone translating from a proven TLA+ spec to code (C, Java, etc.) can easily introduce a typo/bug. Having only done the basic tla+ tutorials (not the OP's

> Someone translating from a proven TLA+ spec to code (C, Java, etc.) can easily introduce a typo/bug. Having only done the basic tla+ tutorials (not the OP's site yet), this is still my biggest roadblock with even trying to use a formal system. The "impedance mismatch", if you see what I mean. Comparing to automated tests, it seems less likely to get both code and tests wrong in concert, than to get a tla+ spec right, and then botch the translation to code. I'm sure it's a faq, and the answer probably boils down to "just try it, and you'll see" ?

thesz 4y ago
Ideally, you would like to have a specification of the system that can be translated into C and TLA+. This way it is harder to introduce bugs - it is hard to compile conditional or arithmetic operator differently in different places and it is trivial to do that manually. If your budget allows, it is worthwhile to invest into translation of C or TLA+ code back into specification code. This way you may run specification checks again against backtranslated specification. And you can do that process to a fixed point where nothing changes, neither (back translated) specification code, nor code generated from specification.
erichocean 4y ago
What I ended up doing was essentially reimplementing TLA+ (and TLC) so that I could code-gen runtime tests from my specs. My TLC implementation enables the "normal" TLA+-style offline checks to determine that you won't violate your invariants, so you can iterate on your specs and find the edges (and fix them). I do the online checks because I don't trust the code, so I check (at runtime) that the code matches the specIfor the exact (runtime) situation that code is being run in. If it doesn't, I hang/abort.