Flying Spaguetti Monster: Verifying protocols with types and finite state machines
summary
Claim: expressive types can verify distributed protocols at compile time. Uses Idris to encode protocols as finite-state machines, Idris type-checked FSMs that reject invalid transitions and model failure paths (vending-machine example rejects “vend before coin”). Uses type providers generating protocol types from a text schema so multiple services share the same checked protocol. Provides a working proof‑of‑concept on GitHub but not production-ready: stable language and docs, limited ecosystem and notable compile-time/memory costs.
AI-written summary · about
chapters (9)
- 0:00Start
- 1:17Who Is the Flying Spaghetti Monster
- 2:25Idris
- 13:41Finite State Machines
- 14:31Finite State Machines Are Often Used to Model Protocols
- 22:36Door Programming Address with Enforced Error Checking
- 24:32Type Providers
- 25:39Fsm Protocol as a Simple Text File
- 29:58Multi-Party Asynchronous Session Types
related talks
46mFinite-state machines? Your compiler wants in!
20mTaming UI complexity with Typed State Machines
50m"No Foul Play" Describing State with Dependently Typed FSMs
21mBeyond Type Checking Building Bulletproof TypseScript Applications
25mMastering UIs with Finite State Machines
37mAtlas Flexible Software Composition using Protocols
21mPolymorphic Typestate for Session Types
01h 04mWhat FP Can Learn From Formal Languages: Towards a Leaner Syntax