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.

  1. 2022/11/01 - PLT An interesting (2-categorical) perspective of theoretical computer science
  2. 2022/04/01 - PLT A proof of symmetry of Leibniz equality by Andras Kovacs
  3. 2021/10/24 - Cubical Cubical boundaries hell (and maybe the next "crisis")
  4. 2021/09/30 - PLT Sigma types demonstrations
  5. 2021/03/02 - PLT Hacking Agda's pattern matching
  6. 2020/09/11 - Cubical Ld Nclusion (4) -- η-rules and codata
  7. 2020/08/15 - MLTT Proving uniqueness of identity proofs from J
  8. 2020/08/01 - PLT Type system with (type) classes and subtyping?
  9. 2020/06/20 - Parser Lexer for two-dimensional syntax (in Alex)
  10. 2020/05/16 - Arend Language extensions of Arend
  11. 2020/05/14 - Arend Functional programming language -- Arend
  12. 2020/05/04 - Arend REPLs with Typed Holes
  13. 2020/03/03 - Tools Thoughts on literate programming tools
  14. 2020/01/19 - PLT Membership proofs and De Bruijn indices
  15. 2019/11/13 - Agda Thinking about tactics and Agda
  16. 2019/10/27 - Misc Blog refactoring alert
  17. 2019/10/14 - Cubical Cold Introduction (3) -- Open Squares can be Capped
  18. 2019/10/01 - Cubical Cold Introduction (2) -- Inductive Types with Path Constructors
  19. 2019/08/20 - Cubical Cold Introduction (1) -- Squares and Diagonals
  20. 2019/08/01 - Cubical Cold Introduction (0) -- Paths and Intervals
  21. 2019/07/14 - PLT Structural typing and first-class case expressions
  22. 2019/06/20 - PLT Type inference under dependent type (meta variables)
  23. 2019/05/22 - Parser Interpreter without an AST
  24. 2019/04/21 - PLT Different styles of equality reasoning
  25. 2019/04/07 - PLT Fragmented Thoughts on Reducible Expressions
  26. 2018/12/06 - Cubical Cubical Agda
  27. 2018/11/16 - PLT The World Over Dependent Types
  28. 2017/11/12 - Kotlin Tricks in using Kotlin `internal`