4 ms·

AppJet.ai can help you in several ways with TLA+: Language fundamentals: Basic syntax, operators, temporal logic, actions, and specifications Modeling techniqu

AppJet.ai can help you in several ways with TLA+: Language fundamentals: Basic syntax, operators, temporal logic, actions, and specifications Modeling techniques: How to represent system state, define actions, specify invariants and temporal properties PlusCal: The higher-level algorithmic language that transpiles to TLA+ TLC model checker: Running specifications, interpreting results, debugging models Common patterns: Modeling mutual exclusion, consensus algorithms, message passing, etc. Practical examples: From simple counters to complex distributed systems If your code is on GitHub you can use our app with it, it will create a safe independant branch "appjet" to work on it. Give it a try and let me know what you think!

ekidd 1y ago
> Common patterns: Modeling mutual exclusion, consensus algorithms, message passing, etc. Practical examples: From simple counters to complex distributed systems I don't know how you composed this response. But it reads more like a laundry list of TLA+-related buzzwords than a response based on any kind of actual experience with TLA+. TLA+ is a weird and obscure niche, easily obscure enough to give most models very serious headaches.
- RUnconcerned 1y ago
  It reads like they asked the AI how it could help and just pasted whatever it said
- skottenborg 1y ago
  I immediately thought this sounded like an LLM reply.
- rvz 1y ago
  exactly. I stopped reading mid-sentence after seeing a cacophony of buzzwords shoved into that AI generated reply. Very disappointed.
  - alexflashdrive 1y ago
    Well, I don't have any idea what's TLA+ is so I just asked the agent and that's it's response yep
    - uncircle 1y ago
      There it is. Like their "AI" companions, the people using them are unable to conceive not knowing something, so they might as well invent anything that sounds plausible, unable to even learn a new concept. Donning-Kruger as a service. I guess that's what defines the 'serious developers' from the rest of us.
      - suobset 1y ago
        DKaaS, gonna start using that more now lol.

ekidd 1y ago

> Common patterns: Modeling mutual exclusion, consensus algorithms, message passing, etc. Practical examples: From simple counters to complex distributed systems I don't know how you composed this response. But it reads more like a laundry list of TLA+-related buzzwords than a response based on any kind of actual experience with TLA+. TLA+ is a weird and obscure niche, easily obscure enough to give most models very serious headaches.

RUnconcerned 1y ago
It reads like they asked the AI how it could help and just pasted whatever it said
skottenborg 1y ago
I immediately thought this sounded like an LLM reply.
rvz 1y ago
exactly. I stopped reading mid-sentence after seeing a cacophony of buzzwords shoved into that AI generated reply. Very disappointed.
- alexflashdrive 1y ago
  Well, I don't have any idea what's TLA+ is so I just asked the agent and that's it's response yep
  - uncircle 1y ago
    There it is. Like their "AI" companions, the people using them are unable to conceive not knowing something, so they might as well invent anything that sounds plausible, unable to even learn a new concept. Donning-Kruger as a service. I guess that's what defines the 'serious developers' from the rest of us.
    - suobset 1y ago
      DKaaS, gonna start using that more now lol.