8 ms·

Just like JavaScript folks like calling their compilers "transpiler", proof assistants folks like calling their compilers "extraction". Essentially it's a compi

by joomy 8mo ago

Just like JavaScript folks like calling their compilers "transpiler", proof assistants folks like calling their compilers "extraction". Essentially it's a compiler from a high-level language to a slightly lower-level, but still reasonably high-level language.

GregarianChild 8mo ago
I would phrase it a little different. Simplifying a bit, a compiler tr(.) translates from a source language L1 to a target language L2 such that semantics(P) == semantics(tr(P)) for all programs in L1. In contrast, and again simplifying a bit, extraction extr(.) assumes not only language L1 and L2 as above, but, at least conceptually, also corresponding specification languages S1 and S2 (aka logics). Whenever P |= phi and extr(P, phi) = (P', phi') then not just semantics(P) == semantics(P') as in compilation, but also semantics(phi) = semantics(phi'), hence P' |= phi'. I say "at least conceptually" above, because this specificatyion is often not lowered into a different logical formalism. Instead it is implied / assumed that if the extraction mechanism was correct, then the specification could also be lowered ...
- joomy 8mo ago
  I'm not entirely sure I fully agree with this definition; it seems somewhat arbitrary to me. Where is this definition from? My usual intuition is whether the generated code at the end needs a complicated runtime to replicate the source language's semantics. In Crane, we avoid that requirement with smart pointers, for example.
  - GregarianChild 8mo ago
    This definition is my potentially flawed attempt at summarising the essence of what program extraction is intended to do (however imperfect in practise). I think extraction goes beyond 'mere' compilation. Otherwise we did not need to program inside an ITP. I do agree that the state-of-the-art does not really full reach this platonic ideal
GregarianChild 8mo 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"?
- joomy 8mo ago
  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.
  - GregarianChild 8mo ago
    Since the point of program extraction from a prover is correctness, I wonder what kind of assertions you prove for STM in Rocq.
    - mzweav 8mo ago
      I'm the other dev of Crane. Our current plan is to use BRiCk (https://skylabsai.github.io/BRiCk/index.html 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 8mo ago
        Thanks. I hope you publish this. I imagine https://github.com/bloomberg/crane/blob/main/theories/Monads/STM.v 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?
        8mo ago

by joomy 8mo ago

GregarianChild 8mo ago

I would phrase it a little different. Simplifying a bit, a compiler tr(.) translates from a source language L1 to a target language L2 such that semantics(P) == semantics(tr(P)) for all programs in L1. In contrast, and again simplifying a bit, extraction extr(.) assumes not only language L1 and L2 as above, but, at least conceptually, also corresponding specification languages S1 and S2 (aka logics). Whenever P |= phi and extr(P, phi) = (P', phi') then not just semantics(P) == semantics(P') as in compilation, but also semantics(phi) = semantics(phi'), hence P' |= phi'. I say "at least conceptually" above, because this specificatyion is often not lowered into a different logical formalism. Instead it is implied / assumed that if the extraction mechanism was correct, then the specification could also be lowered ...

joomy 8mo ago
I'm not entirely sure I fully agree with this definition; it seems somewhat arbitrary to me. Where is this definition from? My usual intuition is whether the generated code at the end needs a complicated runtime to replicate the source language's semantics. In Crane, we avoid that requirement with smart pointers, for example.
- GregarianChild 8mo ago
  This definition is my potentially flawed attempt at summarising the essence of what program extraction is intended to do (however imperfect in practise). I think extraction goes beyond 'mere' compilation. Otherwise we did not need to program inside an ITP. I do agree that the state-of-the-art does not really full reach this platonic ideal

GregarianChild 8mo 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"?

joomy 8mo ago
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.
- GregarianChild 8mo ago
  Since the point of program extraction from a prover is correctness, I wonder what kind of assertions you prove for STM in Rocq.
  - mzweav 8mo ago
    I'm the other dev of Crane. Our current plan is to use BRiCk (https://skylabsai.github.io/BRiCk/index.html 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 8mo ago
      Thanks. I hope you publish this. I imagine https://github.com/bloomberg/crane/blob/main/theories/Monads/STM.v 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?
      - 8mo ago