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