Agreed - with better and lower-cost tooling the tradeoffs get steadily more appealing. Back in 2005ish I put together a panel with Kent Beck of extreme program

Agreed - with better and lower-cost tooling the tradeoffs get steadily more appealing. Back in 2005ish I put together a panel with Kent Beck of extreme programming fame and Martyn Thomas of Praxis, which was doing commercial development using formal methods and Spark/Ada. We were hoping for fireworks but it turns out they were in agreement on a lot of stuff: formal methods need to be used in the context of a pragmatic development process, sometimes iteratively exploring is the right approach, for high reliability you need to complement testing with other techniques like formal methods. Concurrency was one of the examples where there was general agreement that testing and code inspection just isn't enough.