Comment by GregarianChild

Since the point of program extraction from a prover is correctness, I wonder what kind of assertions you prove for STM in Rocq.