Temporal and imperative thinking States, transitions, state machines (automata) Invariants Work in progress Back to Elements