This makes me think of Turing machines which store their own code inside them selves, which you can use for all kinds of interesting proofs. I wish I could find more about this.
Look into Squeak/Smalltalk. It is an operating system/desktop/IDE with self contained compiler.