[GregarianChild]

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

[mzweav]

I'm the other dev of Crane. Our current plan is to use BRiCk (https://skylabsai.github.io/BRiCk/index.html) to directly verify that the C++ implementation our STM primitives are extracted to matches the functional specification of STM. Having done that, we can then axiomatize the functional specification over our monadic, interaction tree interface and reason directly over the functional code in Rocq without needing to worry about the gritty details of the C++ interpretation.

[GregarianChild]

Thanks. I hope you publish this.

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?