\todo{Sidenote: One or more state arguments?}
- \subsection{Explicit state annotation}
+ \subsection[sec:description:stateann]{Explicit state annotation}
To make our stateful descriptions unambigious and easier to translate,
we need some way for the developer to describe which arguments and
results are intended to become stateful.