Using TLA+ for frontend frameworks

[Lucas Müllner]

Dear TLA+ Team,

I'm a full-stack web developer and I stumbled across TLA+ yesterday. I wondered if writing formal specifications for front-end applications written with the Angular framework is reasonable. If so, are there some tutorials on how to do that?

Looking forward to hearing from you.

Best regards,

Ing. Lucas Müllner [he/him]
Full-Stack Software Developer | Certified Professional Software Architect - CPSA-F | IT Consultant

Mobil: +43 664 18 69 524

Email: lucasm...@gmail.com

[Samuel Miller]

Hi Lucas,

I've been using TLA+ for specifying front-end development on a couple projects now. I will try to put some thoughts together in a blog, but a few quick thoughts below.

- Angular can be viewed as a state machine. Modeling user flows through Angular can identify invariants like, "When a user signs up with a phone number, and then exits registration, if they continue registration, the user will eventually provide their email address." Translating workflow diagrams into TLA+ can identify where improper assumptions have been made. 

- Many standard multitier web applications (frontend, backend, DB, maybe there's a cache and/or pub-sub queue) can be modeled with TLA+ in a single specification. This means that we can model data flows in a single file, which can be good for early design and other invariants like, "The system will never store bad data in the database."

I would look into articles[1] which discuss SPA as state machines (the linked article mentions the project xstate [2] which I think could be an interesting companion to TLA+). Learn TLA+ or Pluscal with a focus on states and transitions. I have found that just identifying some invariants in your system can be an important way to understand the project and better discuss with stakeholders. I will try to post some example specifications in the next week or so. 

Cheers,

Sam

[1] https://firstaml.dev/blog/2ldc7qgkjwbg7h2bm3xryc3so6eqb1

[2] https://xstate.js.org/

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CANx93QUz0ZUsogue-%3D314zrHj80z%3Dmc%3DE5DrtGU52tgOK6uWPQ%40mail.gmail.com.