5 ms·

My mind works best with examples, I was about to ask here when I stumbled upon it on the TLA site [0]. The example starts out with a simple piece of code that

by tra3 4y ago

My mind works best with examples, I was about to ask here when I stumbled upon it on the TLA site [0]. The example starts out with a simple piece of code that exposes a bug, then the bug gets fixed and the following question is asked: > Does the issue go away because we’ve solved it, or because we’ve made it rarer? Without being able to explore the actual consequences of the designs, we can’t guarantee we’ve solved anything > The purpose of TLA+, then, is to programmatically explore these design issues. We want to give the tooling a system and a requirements and it can tell us whether or not we can break the requirement. If it can, then we know to change our design. If it can’t, we can be more confident that we’re correct. [0]: https://www.learntla.com/intro/conceptual-overview.html https://www.learntla.com/intro/conceptual-overview.html

gurjeet 4y ago
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]. [1]: https://github.com/hwayne/learntla-v2/pull/13 https://github.com/hwayne/learntla-v2/pull/13
- tra3 4y ago
  Wow, good eye. Presumably this particular bug doesn’t require much other than unit tests.
- NavinF 4y ago
  Huh you’re right! The code and the TLA+ model are different: > if (from.balance <= amount) # guard > if acct[from] >= amnt then
- hwayne 4y ago
  God, that's embarrassing. I just merged your fix.
  - gurjeet 4y ago
    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.
    - phtrivier 4y ago
      > 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.
      - 4y ago
- tpoacher 4y ago
  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 requires a few mental steps in working memory that can easily get missed Whereas isValidTransaction = Current - Withdrawal >= 0 if (isValidTransaction): NewBalance = Current - Withdrawal reads like English, and is hard to get wrong in my view. 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.
  - tpoacher 4y ago
    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 :)
billfruit 4y ago
Does TLA+ system prove the model or does it verify the model by essentially brute-forceing it? AlLoy seem to do the brute force verification using SAT solvers.
- thamer 4y ago
  Yes it is essentially brute-forcing it. Note that TLA+ is the language that the model is written in. The program validating is called TLC, it's a model checker.
- _flux 4y ago
  tlc essentially uses brute-forcing, apalache uses SMT solvers. tlc still has some advantages over apalache in some conditions, but actually I've never even used apalache with my models (I'm still in the practice phase, though).

by tra3 4y ago

gurjeet 4y ago

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]. [1]: https://github.com/hwayne/learntla-v2/pull/13 https://github.com/hwayne/learntla-v2/pull/13

tra3 4y ago
Wow, good eye. Presumably this particular bug doesn’t require much other than unit tests.
NavinF 4y ago
Huh you’re right! The code and the TLA+ model are different: > if (from.balance <= amount) # guard > if acct[from] >= amnt then
hwayne 4y ago
God, that's embarrassing. I just merged your fix.
- gurjeet 4y ago
  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.
  - phtrivier 4y ago
    > 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.
    - 4y ago
tpoacher 4y ago
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 requires a few mental steps in working memory that can easily get missed Whereas isValidTransaction = Current - Withdrawal >= 0 if (isValidTransaction): NewBalance = Current - Withdrawal reads like English, and is hard to get wrong in my view. 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.
- tpoacher 4y ago
  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 :)

billfruit 4y ago

Does TLA+ system prove the model or does it verify the model by essentially brute-forceing it? AlLoy seem to do the brute force verification using SAT solvers.

thamer 4y ago
Yes it is essentially brute-forcing it. Note that TLA+ is the language that the model is written in. The program validating is called TLC, it's a model checker.
_flux 4y ago
tlc essentially uses brute-forcing, apalache uses SMT solvers. tlc still has some advantages over apalache in some conditions, but actually I've never even used apalache with my models (I'm still in the practice phase, though).