Item — HN Reader

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.

3 comments

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