My abandoned PhD was in formal methods and I find dependent types to be pretty neat, but every time I've tried using a dependently typed language for anything it's always been an uphill battle.

When I used to do F# for a living, I was really pushing for using F*, but it was impossible to get any buy-in from coworkers because the learning curve was comparatively steep. I probably should have pushed a bit more, but I figured that I'd potentially have more success trying to push people to use TLA+ (though that was also unsuccessful).

That was unsuccessful as well, and I've come to the (admittedly very cynical conclusion) that software engineers, generally speaking, will never learn anything new if it involves "math" in any way, shape, or form. Once I realized that, it became much easier to lower my expectations of my coworkers.