Contracts are written such that the compiler can diagnose a detected violation if it wants to. However most contracts realistically need whole program analysis to diagnose and no compiler can do that - you want a separate static analysis for that. (this doesn't exist, but there is hope people start writing those)

▲

Cieric 8 hours ago | parent [-]

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.

▲

steveklabnik 7 hours ago | parent | next [-]

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 7 hours ago | parent [-]

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 6 hours ago \| parent [-]
		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...)

▲

bluGill 8 hours ago | parent | prev [-]

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 5 hours ago \| parent [-]
		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.)