[NicoHartmann]

I can't wait to show this to my manager next time he asks why it's taking three weeks to build a simple CRUD app.

"Look, if this guys TLA+ logic struggles to model a 1,500-year-old game without crying over a French pawn-capture rule, you can't expect me to integrate Stripe billing without a few state invariant violations."

[epolanski]

Payments have a gargantuan amount of possible transitions and invariants that are far from trivial to encode.

[NicoHartmann]

I showed this to my manager and his response was: "So... three days?"