In my experience the key challenge is the steep learning curve. You need to understand advanced type theory to really understand what the error messages mean.

In my experience the key challenge is the steep learning curve. You need to understand advanced type theory to really understand what the error messages mean. Another problem is that sometimes there are "obvious" things that you'd like to write where the program itself is small but the proof of correctness isn't as easy. But I'd imagine that in a world of ubiquitous dependent types the software engineering might adapt to that. Either by encouraging you to write things that are easy to prove, or by developing best practices of when it's acceptable to skip a proof.