[joomy]

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]

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