Since the point of program extraction from a prover is correctness, I wonder what kind of assertions you prove for STM in Rocq.
I imagine https://github.com/bloomberg/crane/blob/main/theories/Monads... is the functional specification of STM. I see that you use ITrees. WHat's the reason for not using Choice Trees that tend to be easier for handling non-determinism?
And we're not opposed to choice trees. I personally am not too familiar with them but there's time to catch up on literature. :)
ITrees:
CoInductive itree (E : Type -> Type) (R : Type) : Type :=
| Ret (r : R)
| Tau (t : itree E R)
| Vis {T : Type} (e : E T) (k : T -> itree E R)
ChoiceTrees: CoInductive ctree (E : Type -> Type) (C : Type -> Type) (R : Type) : Type :=
| Ret (r : R)
| Tau (t : ctree E C R)
| Vis {T : Type} (e : E T) (k : T -> ctree E C R)
| Choice {T : Type} (c : C T) (k : T -> ctree E C R)
One can see "Choice" constructor as modelling internal non-determinism, complementing the external non-determinism that ITrees already allow with "Vis" and that arises
from interaction with the environment. (Process calculi like CCS, CSP and Pi, as well as session types and linear logic also make this distinction).