[e-lang] Extensible/meta compilers

[Sandro Magi]

Consider an extensible compiler as described in "Meta-Compilation of
Language Abstractions" [1], 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" [2], 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
transformations?

Sandro

[1] http://lambda-the-ultimate.org/node/2019
[2] http://lambda-the-ultimate.org/node/2387