> So you get complex recursion and inductive definitions baked into the kernel.

It is a pragmatic choice, just like a type system is. I think both of these choices are outdated now that formalisation is fast. What you really want is a simple semantics (what is the semantics of Lean again...?), and build on top of that by verified kernel extensions. Program extraction via proof objects doesn't really work, I don't think anyone does that for real. What you do is you write your program in your term language, and export the meaning of that term as a program. Isabelle does that, too, and you don't need proof objects for that.

In my current version of Practal (Practal Zero) I have a switch for keeping proof objects around as well, in case I want to maybe transform proofs in some reuse scenario. Not sure if I will actually use that, ever, because it would be slow, too. Also, I would rather prove that a certain transformation is correct, and then add this as a kernel extension.