In the computer business, technologies which solve essential problems tend to survive; extensible technologies which solve essential problems tend to grow.
When you look at the largest open source projects, the majority of the actual code tends to come from people working in large companies that depend on the tech stack. Linux, for example, has benefited enormously from IBM's investment of engineering-hours into the project. Ruby on Rails is another example, as are many other web-related frameworks.
The SAGE math environment was a noble effort to displace MAGMA and similar systems, which were benefiting from code contributions from academia, but which remained commercial and not widely available. Later SAGE would evolve to compete with Mathematica and other math suites. Unfortunately, the essential problem being solved was a matter of taste-in-licensing, which is not always essential-enough for a project to take hold.
Coq, Agda, Lean, etc, all solve an essential problem, namely that of providing a theory of higher-order machine-checked proofs. The implementations tend to be extensible, at least for experts. Different segments of the CS and math community are becoming aware of these tools and producing new, impressive artifacts all the time. Overall it's a small community, but it's growing. At the very least, the diversity of artifacts demonstrates that these tools are expressive-enough to be useful in many domains, not just in principle but in practice.
Though it is currently difficult to apply these methods to problems of interest in industry, progress in the field of program logics is real and has lead to real tools (Infer, at least) with real users. The ability to prove properties of programs inevitably leads to the desire to prove properties of fairly technical programs, and in that way a bridge to more abstract, less-computery branches of math will emerge. An ecosystem will form, and pure research which contributes to this ecosystem will begin to take on its own appeal. Other paths to industry-awareness may exist, this is just the one I've been tracking.
In my opinion, patience will be rewarded.
-t