>if it was really that helpful, more people would be applying it and the benefits would speak for themselves. They've been around a long, long time, though, and never caught on - it's hard not to conclude that there's probably a reason.

My impression is that there are actually not that many business domains where a large investment in time and money to get domain logic correctness from 98% to 99.99% correct is actually called for.

Formal methods are a large investment, too. No two ways around it.

Also, while they havent really caught on in general, some of their ideas have made it into modern type systems.