[mmalone]

Have you ever tried to change the protocol used by a running production system? I agree that in greenfield development an agile / iterative approach with a loose process works reasonably well. Once you have a running production system with lots of interconnected components, change gets really hard and really scary. Tools that help manage change in those cases seem useful to me.

Re: formal verification in general, most of the research has been moving towards making it easier to use and giving programmers some of the benefits of verification for free. I don't have any problem with the compiler telling me that my code is going to crash before the crash happens in production. That's unquestionably a valuable thing. Idris (and other languages) are trying to give you those sorts of benefits without reducing productivity or breaking your brain. It might not be there yet, but the progress is exciting.

Finally, both of the problems you identified (complex interactions and edge cases) are things that formal techniques are well suited to address... so I'm not sure how they support your case. Again, the only problem seems to be that the cost outweighs the benefits. But the cost is decreasing quickly.