[siknad]

Lean4 is intended to be both, while Idris is more on the programming side and Agda - one the proof side. Maybe I'm mistaken about Idris, but Agda really doesn't prioritize programming: library handling, ffi, and tooling are all rudimentary.

[epgui]

You may be right— My knowledge of these languages does not run very deep (although I am enthusiastic about them and am learning).