|
|
|
|
|
|
by GregarianChild
149 days 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 |
|
|