I think there are really two types of programmers in this world: programmers who program because they enjoy constrained logic puzzles like the kind you would find in To Mock a Mockingbird, and programmers who enjoy making the computer do cool things. The kind of programmer who gets really deep into type-level programming and formal methods and so on tends to be the former, and the kind of programmer who wants to pragmatically adopt those things, if necessary, but generally opt for the simplest solution that allows them to express what they need to, even if it sacrifices an acceptable (context dependent) level of correctness, or who is willing to move certain checks to runtime instead of compile time to avoid complexity (so contracts and specs instead of dependent types), is the latter.
This is because, when you're programming at the type level, you're often presented with a lot of these really gnarly and interesting puzzles, where you have an extremely limited set of transformations you can apply, and extremely harsh constraints, and it's all heavily abstracted, where you've also got, along the way, to figure out how to encode all sorts of invariants in deeply abstract mathematical terms, which all requires thinking at several levels of abstraction greater than the actual thing you're trying to create, and often requires the same kinds of intuitive leaps as proofs. So they're deeply attractive to the first kind of programmer. And of course, if you're attracted to proofs and abstract mathematical reasoning, perfectly, verifiably, provably correct properties are what are most interesting, feel the most clean and Right and assured, to you. So you're going to want to maximize the amount of proof and verification in the code you write, everywhere you can, and evangelize it to others, both because to you it's just obvious – isn't it just correct engineering, the Right Thing, to write software that's proven correct as much as we can with current knowledge and technology right now? Isn't everything else irresponsible? – and because it's inherently fun, inherently rewarding, for you to do.
Meanwhile, what the second kind of programmer keeps in mind is that types don't exist at runtime. Unless you've completely lost it and are just running programs at compile time – in which case, what's the point? – types don't actually do anything, ever. They don't run, because they don't describe the behavior you want the computer to perform, they only describe generalized and abstract invariants you want the actual behavior to uphold. So the more time you spend on working out logic puzzles in the type system, the less you spend actually writing code that actually directly does anything meaningful to the people who want to use your programs. So if your ultimate goal, the one you keep in mind at all times, is that in the end you want your program to do something useful, then you'll realize that there is actually a tradeoff to highly abstract type system finagling and formal methods and so on. Because while those things do tend to make your program more likely to do the correct thing, but they don't do anything themselves, and usually have a high cognitive load overhead, so the more time you spend on them, the less time and brain space you have to spend on actually making your program do something, and the more time you're spending on checking whether hypothetical code actually does something. So yes, if your goal is to make a computer do something useful, then you're going to need some kind of verification to make sure it actually does the right thing – otherwise you're up shit creek, because you've certainly made the computer do something, but it isn't clear how useful that "something" is, exactly. But the second kind of programmer wants to maximize the amount of time they spend writing code that will actually run and do something useful, so, since working with verification comes at the cost of time and energy and mental space for writing running code, they'll try to minimize doing type system and formal verification stuff as much as possible, with the only factor pushing that mount above zero being the degree to which verified correctness is helpful or necessary for the specific problem at hand.