Proof assistant folks: what's the state of the art these days for extracting code from a proof assistant that's reasonably efficient and not completely disconnected from the proofs?
My understanding (which is probably five or ten years out of date) is that, for example, if you're doing Rocq proofs about programs that use Peano numbers, and you extract your program to, say, OCaml, by default you'd get Peano numbers in OCaml, which of course you don't actually want to use. What are your options?
A bunch of folks are suggesting Lean, so let's see what Lean does for my Peano numbers example:
https://lean-lang.org/doc/reference/latest//Basic-Types/Natural-Numbers/#Nat___zero
"This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation."
So -- assuming I trust the implementation of Lean -- then this is a good answer. (The more "special-casing" and "overriding" it does, of course, the less I trust it. But I trust it more than I would trust my *own* special-casing and overriding, that's for sure.)
Lindsey Kuper
Maggie Zhou