Formal proof languages are pretty neat, but nobody really uses them in the real world. Among the languages that people actually use on a normal basis, even those that claim to have extensive type systems, they still rely on testing for most everything, and once you're relying on testing anyway the type system isn't any kind of real saviour.

There is, perhaps, some segment of the developer community who believe that they are infallible and don't need to write tests, but then have the type system exclaim their preconceived notions are wrong, and then come to love the type system for steering them in a better direction, while still remaining oblivious to all the things the incomplete type system is unable to statically assert. But that's a rather bizarre place to be.