[e-lang] Extensible/meta compilers
smagi at higherlogics.com
Wed Aug 29 13:04:49 EDT 2007
Consider an extensible compiler as described in "Meta-Compilation of
Language Abstractions" , where each abstraction written in the
language is bundled with a domain-specific optimization (DSO). At
compile-time, the compiler detects the DSO, loads it, and the DSO can
then modify the program AST at compile-time to eliminate the abstraction
penalty associated with that particular abstraction.
Clearly this has a significant potential for abuse, since a third-party
optimization could modify your code and leak secrets, invalidate your
invariants, etc. Type safety ensures a limited form of program
equivalence, but it's generally not enough.
Efforts like "Guaranteed Optimization" , where the optimizer is also
a theorem prover can possibly provide a sufficiently strong equivalence
proof, but I'm wondering whether there's a lighter weight alternative.
I can think of ways to limit the transformable code to the portion of
the program which directly uses the abstraction, but there are
potentially a number of whole-program transformations which would be
quite useful, ie. the CPS transform, and some abstractions might not
work properly without a whole program transform.
Any thoughts on how to flexibly control or limit such program
More information about the e-lang