Ask HN: Any sensible usage of TLA+/Alloy for mere mortals?
I am a back-end web developer, and am totally sold to ideas using formal methods to ensure better quality for delivered software, however, it's difficult to - evangelize a new tool to my team, - find a sensible usage, while at the same time, - learning it myself.
So far I have identified following points: - Using TLA+ to model our authentication/2FA process. This isn't a concurrent system, as we would be modelling 1 client's interactions with 1 server, BUT I believe it would be nice to see the system as a whole, I came up with some invariants to check, out of top of my head: "every user is eventually asked for 2FA"?, "every session eventually ends"?, "once created, user can login"?
- Using TLA+ to model business processes; basically describe the state machine of some particular workflow. Not sure yet what invariants to check.
- Using Alloy to model our Database/ORM mapping. Unfortunately, it's already screwed up beyond repair, but at least this would help to quantify how screwed it is. Kinda difficult to justify the time spent, because I don't see myself changing the database schema, too much of a trouble.
Any other suggestions?
P.S: Looks like Alloy is rreeaaallly niche! It's hard to find talks/youtube videos about it, while I have a new video suggested every day for TLA+ at Microsoft & Amazon