K is really cool, but does really give you a compiler? That's the first I heard of that. Do you have (a link to) more information about how it does compilation?