I'm intrigued by the Futamura projections and the possibility of getting a compiler for a programming language "for free" by using partial evaluation to special

I'm intrigued by the Futamura projections and the possibility of getting a compiler for a programming language "for free" by using partial evaluation to specialize an interpreter. It appears that fully automatic theorem proving technology isn't powerful enough for this to work well enough to be interesting. But what about proof assistants? It struck me that using a proof assistant to guide the theorem prover inside a partial evaluator offers an opportunity to repartition the coding task. The idea of "end user programming" always fails because we cannot sufficiently separate the idea of a program that serves as specification (here is what we want done, its a shame that this specification isn't really runable because the implied algorithm is too inefficient (think about PROLOG, where a naive program may well be logically correct, but backtracks itself an exponential runtime)) and a program that describes a tolerably efficient algorithm. The poor end user has enough trouble with writing code that specifies the computation correctly without worrying about computer-sciencey stuff about how the computer should actually go about computing it. If only there was some way the person rewriting the code to make it go fast could do so at one remove. He works with the end user programmer first time through, but subsequent revisions by the end user get rewritten automatically... This was the vision I tried to articulate in https://groups.google.com/d/msg/comp.lang.lisp/5p8oVP5dGbU/VSbp0zBLnaYJ https://groups.google.com/d/msg/comp.lang.lisp/5p8oVP5dGbU/V... but my health has failed and I've not got any further forward :-(