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