I hate to be a downer, but I just don't trust automatic code generation.
Proof automation is nice because proofs are ultimately irrelevant. It doesn't matter what the proof is, only that there is one. With code, it's another matter. If I have to depend on heuristics for it to choose the right option that means that I'll actually have to read and verify whether it chose the correct one. At that point, I feel like I'm not really winning anything over just writing it myself.
It's possible to write a complex specification to ensure the generated code would be correct, but current automation already struggles with generating proofs for hand written code, let alone generating code and verifying it.
Also, it isn't clear to me whether tactics programs are supposed to be kept as code or just used by the LSP which the gif makes it seem like. To me the strongest benefits of tactics are that they can be used to document what the author was trying to do and that using an IDE they can be executed step-by-step. If it's just to be used by the LSP: What is the point of using tactics vs normal metaprogramming?
It's possible to write a complex specification to ensure the generated code would be correct, but current automation already struggles with generating proofs for hand written code, let alone generating code and verifying it.
Also, it isn't clear to me whether tactics programs are supposed to be kept as code or just used by the LSP which the gif makes it seem like. To me the strongest benefits of tactics are that they can be used to document what the author was trying to do and that using an IDE they can be executed step-by-step. If it's just to be used by the LSP: What is the point of using tactics vs normal metaprogramming?