@TaliaRinger@mathstodon.xyz I think type theorists would consider this as rather applied type theory :p But fully agreed! On the positive side (and to toot my own horn a bit) we have not been idle: https://metarocq.github.io/ is the most mature project in the area, but https://github.com/digama0/lean4lean and https://github.com/jespercockx/agda-core/ are also busy, and there's a lot of more fundamental research happening as well to prepare for these project's next steps. The age of verified kernels is coming!