Checkout Lean, the lead developer also started Z3 . Lean 3 is implemented in C++ and apparently is much faster than Coq. They are in the process of implementing Lean 4, which will feature native code generation and might become one of the first practical dependently typed programming languages.