Hacker News Reader

Comment by tra3 | Hacker News Reader

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

View on HN

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

Wow, good eye. Presumably this particular bug doesn’t require much other than unit tests.

Huh you’re right! The code and the TLA+ model are different:

> if (from.balance <= amount) # guard

> if acct[from] >= amnt then

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.

> 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.

> 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.

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.

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 :)

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.

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.

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).

Reply on news.ycombinator.com