Nobody builds web servers in Coq, but they do in Haskell, which I believe has some form dependent types coming. That's the kind of moving from niche languages to increasingly mainstream ones I mean. From there, maybe eventually it gets refined and even later properly mainstream.

Sorta, but not precisely. But it's the kind of progress I see as encouraging for the future of formal methods in mainstream software development.