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.

- A proof of symmetry of Leibniz equality by Andras Kovacs
- Cubical boundaries hell (and maybe the next "crisis")
- Sigma types demonstrations
- Hacking Agda's pattern matching
- Ld Nclusion (4) -- η-rules and codata
- Proving uniqueness of identity proofs from J
- Type system with (type) classes and subtyping?
- Lexer for two-dimensional syntax (in Alex)
- Language extensions of Arend
- Functional programming language -- Arend
- REPLs with Typed Holes
- Thoughts on literate programming tools
- Membership proofs and De Bruijn indices
- Thinking about tactics and Agda
- Blog refactoring alert
- Cold Introduction (3) -- Open Squares can be Capped
- Cold Introduction (2) -- Inductive Types with Path Constructors
- Cold Introduction (1) -- Squares and Diagonals
- Cold Introduction (0) -- Paths and Intervals
- Structural typing and first-class case expressions
- Type inference under dependent type (meta variables)
- Interpreter without an AST
- Different styles of equality reasoning
- Fragmented Thoughts on Reducible Expressions
- Cubical Agda
- The World Over Dependent Types
- Tricks in using Kotlin `internal`