> 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

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