Made in Heaven
We say that a language is compiled if the translator analyzes it thoroughly (rather than effecting some
"mechanical" transformation), and if the intermediate program does not bear a strong resemblance to the source.
These two characteristics—thorough analysis and nontrivial transformation—are the hallmarks of compilation.
We say that a knowledge point is comprehended if you analyze it thoroughly (rather than echoing
what the books say), and if the concept generated in your brain does not bear a strong resemblance to the text.
These two characteristics—thorough analysis and nontrivial transformation—are the hallmarks of comprehension.
Update: My recent writing are mainly about the Aya prover, which can be found at its website.