[didibus]

I'm sure there's a branch of programming where that would be amazing, but in my experience, I've never had major bugs due to my client and server implementing their protocol wrong.

In fact, I question most of the value of formal verifications for non critical software. Most of the problematic bugs that make it through in my experience are either a complex combination of multuple parts of the system interacting together in a way that doesn't end up behaving the way it was intended, or programmers implementing the wrong thing on edge cases.

[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.

[haskellandchill]

I have 8 years of industry experience and feel the exact opposite. When programming in Ruby I am forced to not fully express the concepts in my head. We do TDD but our tests are humorously thin; typically covering none, one, many. Idris proofs are tricky but more automated and powerful than writing tests. And I can still write tests in Idris.

To go beyond "protocols", UI form data to server response back to UI display in a web app is a source of major bugs. So many things are broken. Recently I had to add a spurious lap infant to book a flight due to JavaScript template being broken when rendering 0 children.

[vijucat]

What happens if you try to book 9007199254740993 spurious lap infants? Just curious.

I'd love to QuickCheck the diapers out of this method.

[codygman]

spurious lap infant?

[haskellandchill]

True story: https://i.redd.it/lc84fv1lrv2z.png

[mej10]

You seem to just be thinking about low level network protocols.

The idea of a protocol in this sense encompasses pretty much any communication between things. This includes web service calls, user input via a UI, transactions between multiple systems, or even modules within the same program.

[Karrot_Kream]

I've encountered so many bugs because of mismatches between server and client APIs, it's not even funny. Even then it remains a persistent problem, as evidence with changing Thrift schemas forward.

[_0w8t]

For write once and forget type of code like a website implemented by a contractor or throwaway code in Jupyter notebooks, the formal verification has a negative value indeed. For anything complex under maintenance ability to see that code behaves as expected in the edge cases without running it is invaluable.