I found this about implementing Imp[0] in Coq (which is the language he writing tree-sitter for) to be interesting as well.

[0]: https://softwarefoundations.cis.upenn.edu/lf-current/Imp.htm...