Rendered at 13:45:37 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
listless 20 minutes ago [-]
I can’t understand any of this. It’s saying everything and nothing at the same time. Whatever TLA+ is this article makes it sound like the most tedious and academic thing ever.
stevefan1999 2 hours ago [-]
I indirectly use TLA+ through https://github.com/quint-co/quint. I added instructions that "before you implement any feature, please use Quint to model it and make sure no counterexample for the system as a whole, reiterate the design with Quint as well and make sure your documents and implementation follows the formal model and docs".
The result, while takes much longer, is quite magical. A lot of transaction and atomic bugs were found and fixed just by having such simple instruction alone.
However, sometimes it is not all magical especially around external resources. Cloudflare, unfortunately, sometimes have hiccups on D1 and KV with timeout, which is more or less a force majeure.
Fortunately, that means I will have to model the action as a binary event, that the transaction may not complete as we would have thought guaranteed, and by add extra guard around it, so that the state would have to be retried.
I was able to workaround it like that so far. Keep in mind the more conditions and constraints, the beefier your CPU might need since it is on the scale of NP
bsenftner 3 hours ago [-]
Took 10 minutes to find this: TLA+ is a formal specification language developed to design, model, document, and verify reactive systems.
mkl 14 minutes ago [-]
It takes about 5 seconds to open Wikipedia and type "TLA+".
noosphr 2 hours ago [-]
TLA+ is what unit testing looks like when a mathematician designs it.
stroebs 1 hours ago [-]
17 mentions of “TLA+” before defining the acronym.
brookst 20 minutes ago [-]
Which is ironic and funny given the other common use of those letters.
The Intel paper shows how TLA+ was applied as a step prior to writing the hardware description. I'm not sure if it caught on, it seems like other tools are used nowdays, does anyone here in the VLSI industry know?
baq 19 minutes ago [-]
the secret's out, but I think I'm still in a minority which has alloy models in addition to TLA+ ones
lisp2240 3 hours ago [-]
Take a writing class. This was painful to read.
rsrsrs86 2 hours ago [-]
Yep. Unreadable
pelagicAustral 3 hours ago [-]
Hahaha this is so funny... people here get slammed all the time of using AI for writing and here be, just someone writing his way through Internet history and gets slammed for it just the same... you can't hardly win with an audience like this... haha
cryptonym 2 hours ago [-]
You can be bad at writing with or without AI.
pona-a 7 minutes ago [-]
[delayed]
torutofu 40 minutes ago [-]
the jump from reading examples to writing a useful invariant is still the hard part
alexnewman 25 minutes ago [-]
I did a lot of distsys work
With tla+. I still think it’s the best use. It’s really hard to make sure your code matches what you prove.
Time to discover communicating sequential processes instead :P
usrnm 4 hours ago [-]
That stuff gets rediscovered all the time, the latest example probably being golang
Yoric 3 hours ago [-]
Nah, jump straight to pi-calculus.
miranaproarrow 4 hours ago [-]
wait this is new to me so is this like a different kind of tla?
als0 4 hours ago [-]
I've always thought CSP as a robust design pattern where you have no shared state between components and they must communicate with each other using message passing. It also requires synchronous communication (rendezvous-style). If you follow those rules you can have a pretty robust system. Aside from these abstract rules, CSP has more formal research (algebra) but I'm not sure if there are any decent tools available.
TLA gives you a full toolbox and in theory can model whatever you can express. That's very different from a design pattern.
azaras 4 hours ago [-]
I am learning TLA+ but I do not know CSP, is CSP better?
The result, while takes much longer, is quite magical. A lot of transaction and atomic bugs were found and fixed just by having such simple instruction alone.
However, sometimes it is not all magical especially around external resources. Cloudflare, unfortunately, sometimes have hiccups on D1 and KV with timeout, which is more or less a force majeure.
Fortunately, that means I will have to model the action as a binary event, that the transaction may not complete as we would have thought guaranteed, and by add extra guard around it, so that the state would have to be retried.
I was able to workaround it like that so far. Keep in mind the more conditions and constraints, the beefier your CPU might need since it is on the scale of NP
The Intel paper shows how TLA+ was applied as a step prior to writing the hardware description. I'm not sure if it caught on, it seems like other tools are used nowdays, does anyone here in the VLSI industry know?
https://news.ycombinator.com/item?id=48287718
With link to pdf, github
TLA gives you a full toolbox and in theory can model whatever you can express. That's very different from a design pattern.