contracts are intended to document hoare logic. i.e. pre, post, invariant.

They can be compile time if the compiler can verify them statically (where they become a noop), runtime otherwise, or disabled entirely if you can't prove them statically but don't want the overhead cost.

Realistically contracts will gradually evolve towards static/compile time asserts as tooling improves.

And like the blog post states, contracts are explicitly not input validation. They are there to encode what you expect and what you don't internally in your code rather than just documenting those pre/post/invariant conditions in comments.

▲ cogman10 9 hours ago | parent | next [-]

> Contracts are explicitly not input validation. They are there to encode what you expect

The line between what's "input validation" and what's "What you expect" is very muddy. Input validation is a statement of "this is input I expect".

Is it input validation to say a string must be at least some length characters? What if that string is a password? What if it's an MD5 sum?

It SHOULDN'T be used for input validation but it will be. And almost certainly the person that does use it for input validation will argue that they were just laying out expectations.

▲

spider-mario 5 hours ago | parent | next [-]

> The line between what's "input validation" and what's "What you expect" is very muddy. Input validation is a statement of "this is input I expect".

> Is it input validation to say a string must be at least some length characters? What if that string is a password? What if it's an MD5 sum?

Think of it this way: pre-conditions are what the function assumes to be true when it’s called. If it would not be justified to make that assumption at the point where the function is called, it is the responsibility of the caller to perform a runtime check to ensure that it applies. So you might well have a precondition at the level of the function and an explicit check of the exact same condition on the caller side to ensure that it’s respected. If the caller fails to ensure that the condition is fulfilled, and the precondition thereby trips, that’s a programming error.

	▲	OneDeuxTriSeiGo 2 hours ago \| parent [-]
		Yep this is exactly it. It's a sanity check that enforces the invariants so that when someone else violates those invariants and they don't know what went wrong they can easily debug it.

▲

OneDeuxTriSeiGo 8 hours ago | parent | prev [-]

> Is it input validation to say a string must be at least some length characters

Yes. Yes it is. Input validation should happen at the public API and then contracts after that.

Contracts are very explicitly for things you don't want to ever see happen. They are "something went wrong".

So your API would accept a function that handles input validation and maybe has its own contract for things it explicitly doesn't handle but then internally you use contracts to enforce that the string is already input validated and you don't have to enforce edge cases.

▲ nickorlow 8 hours ago | parent | prev | next [-]

> They can be compile time if the compiler can verify them statically (where they become a noop)

This only happens during constant evaluation. For example, the following could be determined statically, but compiles w/o error on gcc

int add_nums(int x, int y)

    pre(x >= 0)

    pre(y >= 0)

{

    return x + y;

}

int result_rt = add_nums(-1,-1); // no compile error

▲

bluGill 8 hours ago | parent [-]

It compilers on the current gcc version (or at least the one you tested). Future gcc can make it an error.

▲

nickorlow 8 hours ago | parent | next [-]

Yes, though that wouldn't be consistent w/ the standard

▲

bluGill 8 hours ago | parent [-]

The standard doesn't require compilers find all such cases. The standard allows it, but doesn't require it. There are many known cases where the compiler cannot find a case (at least not in a reasonable amount of time)

	▲	nickorlow 7 hours ago \| parent [-]
		The consequence of not being required in the standard is that compilers may not implement it and if they do, they will likely have different implementations/functionality

▲

cyberax 6 hours ago | parent | prev [-]

That's like compiling with -Wall. Stuff will keep breaking randomly, so people will just disable it.

	▲	bluGill 4 hours ago \| parent [-]
		Some people. Most projects I know of build -Wall and fix all the errors. Developers all run - Error. 30 years ago this was madness but compilers are good about fixing false positives and so it is reasonable. It isn't reasonable to expect downstream (i.e. Debian) to fix warnings but developers generally do for code they maintain.

▲ 8 hours ago | parent | prev | next [-]

[deleted]

▲ 9 hours ago | parent | prev | next [-]

[deleted]

▲ rramadass 4 hours ago | parent | prev [-]

https://news.ycombinator.com/item?id=50108112