[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?

[joomy]

Our 2 page extended abstract was more like a preannouncement. We hope to have a draft of the full paper by the end of the year.

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. :)