"What I would be terrified of in Coq is some tiny change in business requirements ends up pulling the linchpin out of some fundamental premise way down at the bottom of your stack of proofs, this forcing you to go and fix everything."

I'm still wondering how often that will be a problem if high-assurance methods get more adoption. I'll note it's mitigated a lot by the advice we give about where to apply formal methods:

1. Highly critical stuff.

2. That doesn't change at a fast pace.

3. That's known to be verifiable with existing methods in the time frame needed. As in, you want pre-verified components or it to be really similar to past projects.

One thing to support No 3 is to have straight-forward, sequential code that's composed in a hierarchical way with clearly-specified interfaces. You'll mostly be just be verifying behavior of individual components. A change at the bottom will be isolated into that module. Then, you prove the integration of whatever calls it. Then what calls that. With the proper structure, you dramatically reduce the work required with the reverification.

" I don't think Coq leaves much room for being pragmatic about test coverage like that."

People that use it often try to use it for everything because formal verification is their job. In industry, you use it where it makes sense. That might be most critical component which is also pretty simple. Actually, most in industry use model-checkers (i.e. SPIN, TLA+) and languages with solvers (i.e. Frama-C, SPARK Ada) for verification. That minimizes their work. The most-adopted methods, though, for the $5 bugs are software inspections (i.e. checklists), static analyzers, test generation from source, and fuzzing. I strongly recommend using them in order of lowest-cost and fastest results to highest-cost, hardest results to avoid wasting time.

> What I would be terrified of in Coq is some tiny change in business requirements ends up pulling the linchpin out of some fundamental premise way down at the bottom of your stack of proofs, this forcing you to go and fix everything. Sort of the mother of all brittle testing scenarios.

Isn't the same true for static typing? One small business requirement changes, you change a foundational type, and suddenly all your code needs to adapt.

Of course this is true with dynamic typing too, but at least you don't know.

> Isn't the same true for static typing? One small business requirement changes, you change a foundational type

Business changes are usually changes in logic, not in types. So it's mostly "our cashback is now calculated in percentage of the sum, not as a fixed sum" etc. Of course, this may still have repercussions through the entire system. I don't know how it would work in Coq (I don't know Coq :) ).

> Business changes are usually changes in logic, not in types.

Types _are_ logical propositions. In languages like Coq they are more expressive, and it's easier to leverage them as a way to constrain your implementation. Of course it's just a model, and there can be bugs in the specification, so it's not a silver bullet.

> types are propositions

ML and Coq types, yes. Java, C types? Not so much.

Call them "illogical propositions".

I guess. My experience has been that it's more a case with, for lack of a better term, "old school" OOP.

SOLID helps a lot with that sort of thing. Avoiding inheritance like the plague helps a lot. I slightly hate that I said old school, because Smalltalk-style tell-don't-ask helps a lot.

I think that the idiomatic ways of structuring code in the ML family of languages help the most, because they tend to be pretty radical about limiting scope of visibility. But they also tend to make more of a muddle of things than they're worth in algol-style languages.

> What I would be terrified of in Coq is some tiny change in business requirements ends up pulling the linchpin out of some fundamental premise way down at the bottom of your stack of proofs, this forcing you to go and fix everything.

To be a bit facetious: What I would be terrified of in software development is some tiny change in business requirements ends up pulling the linchpin out of some fundamental premise way down at the bottom of your stack of functions, this forcing you to go and fix everything.

There is good proof engineering and bad proof engineering, just like there is good software engineering and bad software engineering. (If only all of us could agree on what exactly is good and bad in either ;-)). Coq has all sorts of modularity and abstraction facilities that you can use to build an architecture that is hopefully resilient to change.

But yeah, it's not perfect. Particularly because proofs are not always like unit tests: At the lowest level you prove things about actual implementations of functions, not just their behavior. In tricky cases, changing a low-level function does mean that you may have to change a lot of proofs. How to avoid this is still an open problem.

This really depends on what you're doing. I suppose most of the code I've written in the last two decades wouldn't have profited from using coq. BUT then there's CompCert, an optimizing compiler written in coq [I'm affiliated, but not working on it directly]. If you're building safety critical stuff (like in failure == people die) something like this might be interesting.

Of course, for a C compiler the requirements are less prone to change than e.g. some SAP-style business application. As a dev, coq is just another tool in your belt and being a good dev means knowing when to use what tool.

I think that’s to a certain extent a matter of approach: we’ve discovered over time that certain approaches e.g. huge business logic inheritance trees are susceptible to this problem, whereas others e.g. list comprehensions, grouping constructs, functors &c aren’t.

So I’m sure you _can_ build something in Coq that is fragile as you describe, but I feel sure that there are alternative approaches that won’t be as brittle.