Yes Idris was meant to write regular code. F* is also meant to write regular code

But I think that the theorem prover that excels most at regular code is actually Lean. The reason I think that is because Lean has a growing community, or at least is growing much faster than other similar languages, and for regular code you really need a healthy ecosystem of libraries and stuff.

Anyway here an article about Lean as a general purpose language https://kirancodes.me/posts/log-ocaml-to-lean.html