The internet discovers TLA+. Now what?

Discussion (9 Comments)Read Original on HackerNews

peterus•14 minutes ago

Real world applications of TLA+: https://foundation.tlapl.us/industry/index.html.

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?

scrubs•about 1 hour ago

See:

https://news.ycombinator.com/item?id=48287718

With link to pdf, github

lisp2240•35 minutes ago

Take a writing class. This was painful to read.

fizlebit•about 2 hours ago

Time to discover communicating sequential processes instead :P

Yoric•10 minutes ago

Nah, jump straight to pi-calculus.

usrnm•about 2 hours ago

That stuff gets rediscovered all the time, the latest example probably being golang

miranaproarrow•about 1 hour ago

wait this is new to me so is this like a different kind of tla?

als0•about 1 hour 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•about 1 hour ago

I am learning TLA+ but I do not know CSP, is CSP better?

The internet discovers TLA+. Now what?

⚡ Community Insights

Discussion (9 Comments)Read Original on HackerNews