I'm on the practical side of things and have dabbled quite a bit with languages like Idris, I think we are mostly far from using them because of ergonomics.

Even in Scala (which is a very advanced language, but still far behind Idris) I deliberately don't use certain type-level features because it increases the compilation times too much (even with incremental compile!). It's very sad, but this is reality.

So, the problem isn't really that we need to "invent airplanes" - we already have them! What we need to do is make them usable and affordable by everyone.

I see more and more languages trying to add type-level features or try to embed other languages like Prolog-like ones into them. I hope that gets traction and becomes ergonomic, otherwise no one will use it in practice.

I agree; I would say that most can be taught to people without advanced math/logic degrees/backgrounds, but because the tools are created by (and usually for) people with formal verification majors), they are just quite bad ergonomically as you say. I think we are in a good place of making it these types of proofs easier and faster more mainstream effort, not just one professor and their students, is put behind it. I believe AI will play a part here.