Hacker News Reader

Comment by bluGill | Hacker News Reader

If I have more experience than you that means you have no experience at all. I've never used contracts in anything (not even a toy). I've been following contracts in hopes that they can be the next step in my quality journey, but I have no real world experience myself.

By whole program analysis I mean you need the entire call tree of a function - stopping only when you can validate that the range of values is constrained to legal values. For some functions this is really simple, while for others the whole flow can be thousands of functions.

View on HN

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

Yeah, that sounds like the system I rediscovered. The only other thing I'm adding to try and lean more into that system are assertions(?) that are in the middle of a function, that can basically break it up into blocks on their own where the first block proves it true and the second block assumes it's true. So effectively the same thing as breaking it into 2 smaller functions. My main thing right now is, I'm fairly certain there is something wrong with my compiler, I'm a basically a novice in contracts, I'm intermediate in compilers, I'm a novice on SMT proofs, and I wrote the whole thing at this point using AI just to test an idea. So I'm just trying to throw everything I can at it to try and break it. I need to start building it again from scratch (without AI) so I can truly understand where it might break and what doesn't work.

Reply on news.ycombinator.com