When modeling problem domains, we collect different possible states, legal transitions between states, and relevant data for each state. Finite-state machines emerge. To verify that programs are constructed correctly, and to have a living machine-verified documentation, we should let the compiler in on our trade secrets. In this talk we will look at motivations and examples of encoding finite-state machines, using the expressive type systems of Haskell and PureScript.