> and then be able to compose the things you’ve proved separately

This has always struck me as the really challenging, problematic part about correctness proofs. I've no formal training in this area (sadly), but how does one go about being able to just compose your proof components? Often as not, that seems like a pipe dream - http://queue.acm.org/detail.cfm?id=2889274