8 ms·
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 g
by 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 agoThis 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