> Formal verification is still too limited to be useful for most app developers

Limited formal verification is useful to most app developers. Consider a simplistic system that requires you to specify variables as strings or integers. You've almost certainly used a language that can express that before. Being able to formally verify that you haven't tried to stuff a string into an integer in order to give your editor the squiggles is a productivity enhancer. Or used to be in the pre-vibe coding days, at least; who knows anymore.

Your tests will eventually tell you the same thing, that is true, but the industry has decided that there is little downside to having at least some degree of formal verification and a whole lot of upsides. The question is always: where do the returns diminish? This is where you get the silly commentary on HN with the Rust guys crying out that Go isn't expressive enough and the Rocq guys laughing at it all.