Well, all the naysayers could also do some research instead of being as dismissive as they are. Here's an example of actual use of formal methods: http://lamport.azurewebsites.net/tla/amazon.html
Why aren't they used more widely? Because when people hear"math", they immediately think of it as academic. It would also be overkill for most projects.
TLA is one of the systems that are actually very practical. You can go up or down as many abstraction layers as you need . There's a great introduction written by @pron on his blog [1].
However, it's worth pointing out that you don't magically get the final program out of the TLA proof. The proof only works for the abstraction level that you chose to write it at.
