Chapter 14. Dependent state machines: handling feedback and errors
This chapter covers
- Handling errors in state transitions
- Developing protocol implementations interactively
- Guaranteeing security properties in types
As you saw in the previous chapter, you can describe the valid state transitions of a state machine in a dependent type, indexed by the required input state of an operation (its precondition) and the output state (its postcondition). By defining valid state transitions in the type, you can be sure that a program that type-checks is guaranteed to describe a valid sequence of state transitions.
You saw two examples, a description of a door and a simulation of a vending machine, and in each case we gave precise types to the operations ...
Get Type-Driven Development with Idris now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
