Comment by GregarianChild
25 days 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 ...
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.
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