I noticed a bug in the example, and thought that was the bug TLA+ would be used to solve. Apparently, that's a real bug, and the rest of the doc does not address it. So I proposed a fix for it [1].
back
4 comments
God, that's embarrassing. I just merged your fix.
Take it easy; it's a proof that you're only human :-)
This bugfix brings up 2 good points.
1. Using TLA+ is no silver bullet to writing bullet-proof code. Someone translating from a proven TLA+ spec to code (C, Java, etc.) can easily introduce a typo/bug. I wish there was a translator that'd convert your TLA+ to code in a language of your choice.
2. Say what people may want about centralization (Git vs. Github, etc), this successful micro-collaboration was enabled by this centralization. Someone posts a link to a book/article, someone else posts a deep-link to some example code, yet another person finds bug in the said code, hunts down the Github link, uses Github's in-place edit feature (no (`git clone` + fix + `git push`)) and submits a merge-request, the author merges the fix (and smacks head :-). All this was kicked off by a conversation on HN, a center/hub for conversations.
> 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" ?
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.
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.
> All this was kicked off by a conversation on HN, a center/hub for conversations.
This isn't a good argument for centralization. Yes, obviously we need to meet in the same "place" for this to happen, but this "place" could just as well be an identifier, for instance a Matrix room. There is no need for the server architecture to be centralized.
Additionally, I don't find your example of in-place editing being much better than `git clone` + fix + `git push` to be very motivating. At best, that's an UX issue, not an inherent benefit of centralization.
The rest of your points actually stand and I agree with them, even when we ignore the misguided call for centralization.
> Take it easy; it's a proof that you're only human :-)
No, it's not proving anything. Github Copilot could have definitely made the same mistake.
For me this is also a point about writing code that can easily be mentally translated to human language.
It might seem simple enough, but this bug shows that
if (Current < Withdrawal): Current -= Withdrawal
Whereas
isValidTransaction = Current - Withdrawal >= 0
if (isValidTransaction): NewBalance = Current - Withdrawal
In the first case, the reader is expected to do mental math (albeit easy) in order to verify correctness. Whereas in the second, they're only expected to read a logical statement and confirm that the logic checks out.
Increment this counter by one (by upvoting this comment) if you thought I was exaggerating, but hadn't immediately noticed the same bug as the one OP reported in my top example :)
Huh you’re right! The code and the TLA+ model are different:
> if (from.balance <= amount) # guard
> if acct[from] >= amnt then
Wow, good eye. Presumably this particular bug doesn’t require much other than unit tests.