alt Hacker NewsAh damn, okay. Long functions with a lot of sub calls is a known problem. I've been able to work around some of the issues tried to them by making every function an independent "compile unit." and then solving them each individually in the SMT solver. My experience in contract based programming is still relatively light, I won't lie there. The most I've had to do with contracts was ada, and even then it wasn't much. Everything else has been self enforced in languages without explicit support (and hence no compile time checking.)
I'm no expert. my understanding though is that one of the reasons for contracts is solvers cannot possibly handle all the possible states of a program. if you can throw a contract in places they can break your whole program into subsets. That is, when analyzing a function and everything it calls, it just assumes the contract holds. And if everything works correctly according to contract and doesn't crash, well, they know that function is satisfied. Then they don't need to go back and say, well, everything calling that previous function only needs to meet the contracts, they don't need to prove everything that function calls is correct. This they can only do a subset of the full program analysis prove the whole program.