That's a good software pattern in general, and as you use more and more powerfully typed languages, the Coq analogy becomes even more obvious. If you write smal

That's a good software pattern in general, and as you use more and more powerfully typed languages, the Coq analogy becomes even more obvious. If you write small modules, it's easier to statically prove more behavior. Then all you need is to compose the modules, and thanks to composition being a small, well-defined, and lawful operation, the correctness of your program becomes the sum of its proofs :)