8 ms·

You sounds like you have more experience than me in this space (specifically contracts). I'm curious if you have any examples right off hand that would need who

by Cieric 18d ago

You sounds like you have more experience than me in this space (specifically contracts). I'm curious if you have any examples right off hand that would need whole program analysis. I need more examples to throw at my toy language that's not just another lock free work stealing queue.

bluGill 18d ago
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.
- Cieric 18d ago
  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.)
  - bluGill 18d ago
    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.
    - Cieric 18d ago
      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.
steveklabnik 18d ago
C++ contracts are not a compile-time construct, they're a runtime construct. Take the example from the article. The contract trips at runtime, not at compile time.
- bluGill 18d ago
  The only required enforcement is runtime (even then it is optional). However nothing stops the compiler from detecting a violation at compile and time failing because of an error (or perhaps warning?) There is a lot of interest in static analysis enforcing contracts, but this will likely require some additions to the contract specification.
  - steveklabnik 18d ago
    I mean, what stops it is > this will likely require some additions to the contract specification. You need a lot more machinery to move this stuff to compile time, and not everything can be checked at compile time. The first example in the post would require you to validate that a <= v's len before indexing in order to be evaluated at compile time, for example. (Which of course is a runtime check anyway...)

by Cieric 18d ago

bluGill 18d ago

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.

Cieric 18d ago
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.)
- bluGill 18d ago
  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.
  - Cieric 18d ago
    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.

steveklabnik 18d ago

C++ contracts are not a compile-time construct, they're a runtime construct. Take the example from the article. The contract trips at runtime, not at compile time.

bluGill 18d ago
The only required enforcement is runtime (even then it is optional). However nothing stops the compiler from detecting a violation at compile and time failing because of an error (or perhaps warning?) There is a lot of interest in static analysis enforcing contracts, but this will likely require some additions to the contract specification.
- steveklabnik 18d ago
  I mean, what stops it is > this will likely require some additions to the contract specification. You need a lot more machinery to move this stuff to compile time, and not everything can be checked at compile time. The first example in the post would require you to validate that a <= v's len before indexing in order to be evaluated at compile time, for example. (Which of course is a runtime check anyway...)