Haskell and others have pretty much proved it's possible in practice as well. But from my experience the cure is worse than the disease. Wishing that software was as formal as math is one thing. Pretending it is leads nowhere worth going.

I have most of my feet in the C++/Common Lisp camps these days. Where you accept that the world is a messy place with complex problems that don't fit neatly into labeled boxes, and use the most powerful tools you can think of to deal with it.