Comment by rafaelRiv

I would say that the value of dependent types in software engineering isn't in proving all code correctness. As a user pointed out in the idris2 Zulip, most programs using dependent types don't have, and shouldn't have, proof of validity for the entire program. Instead, you simply get more correct code by construction, and I think that's the whole point.

I'm currently developing a unikernel in idris2, and the experience is very pleasant (unfortunately, I'm not quite ready to share it yet).