The internet discovers TLA+. Now what?

(reasonable.io)

19 points | by matt_d 5 hours ago

5 comments

  • peterus 9 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 48 minutes ago
  • lisp2240 30 minutes ago
    Take a writing class. This was painful to read.
  • fizlebit 2 hours ago
    Time to discover communicating sequential processes instead :P
    • Yoric 5 minutes ago
      Nah, jump straight to pi-calculus.
    • usrnm 1 hour ago
      That stuff gets rediscovered all the time, the latest example probably being golang
    • miranaproarrow 1 hour ago
      wait this is new to me so is this like a different kind of tla?
      • als0 58 minutes 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 1 hour ago
      I am learning TLA+ but I do not know CSP, is CSP better?
  • Marbleferry815 2 hours ago
    [dead]