I would love to be able to do more formal proving of programs in practice, but I 100% agree with you. A lot of what the advanced typing crowd seem to be doing i

I would love to be able to do more formal proving of programs in practice, but I 100% agree with you. A lot of what the advanced typing crowd seem to be doing is to re-invent programming but at the type level, and it's unclear to me why that should count as progress. It reminds me uncomfortably of C++ template metaprogramming -- and for good reasons, C++ has made steps towards replacing that with statically evaluated expressions written in regular syntax. My gut feeling is that the right way forward is to have a fairly standard type system visible in the source language augmented by contracts written in regular code. Basically a slight augmentation of assert(). A formal prover could internally reason about an extended type system where those contracts are automatically lifted to the type level if that helps for some reason, but programmers wouldn't be bothered with it. This seems unlikely to be a genuinely novel idea, so I'd be curious to hear whether systems like that already exist.