Comment by GregarianChild
1 month ago
I have another question, the abstract of your paper says that you "provide concurrency primitives in Rocq". But this is not really explained in the text. What are those "concurrency primitives"?
1 month ago
I have another question, the abstract of your paper says that you "provide concurrency primitives in Rocq". But this is not really explained in the text. What are those "concurrency primitives"?
We mean Haskell-style software transactional memory (STM). We call it a primitive because it is not defined in Rocq itself; instead, it is only exposed to the Rocq programmer through an interface.
Since the point of program extraction from a prover is correctness, I wonder what kind of assertions you prove for STM in Rocq.
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.
5 replies →