Archived tweet #9309 from the @leastfixedpoint Twitter ArchiveTactics (in Coq) are opaque to read. Conjecture: this is because a tactic is a fn of type *ProofState -> *ProofState; that is, an imperative command. It's confusing in the same ways that traditional imperative languages are, but to a different degree.
