I haven't seen any good examples of contract preconditions that I would actually want to use. What I've seen is stuff like

  double safe_sqrt(double x)
    pre(x >= 0.0)
    post(r: r >= 0.0)
  {
    return std::sqrt(x);
  }

Preconditions violate the principle of "make invalid types unrepresentable" but look like they're helping. They are basically a oneoff extra specific type that (if the state you're checking is worth checking at all, it must be representable in the actual argument's type) contradicts the actual argument's type. So why not change the argument's type directly?

Because it's hard, or not possible, for the same reason that most of these preconditions aren't generally statically verifiable.

Suppose your precondition is x > 5. Statically, you can stop someone from directly passing a literal <= 5, detect locally declared variables assigned to numeric literals and do the same. But to generally infer whether any argument satisfies specific properties quickly gets extremely complicated, because how can you generally verify that the calculations done to a const or literal within the caller's scope guarantee certain properties about the output, without actually performing the calculation? You can come up with cases where you only add to an int and you see it was initialized to 0, so you know it's never < 0 barring underflow. Those are the easy cases

If the caller is passing in something derived from their own arguments, or from I/O, all bets are off. All you know is that the argument has a type, and its value was derived from unknown inputs. So you need a runtime check to actually assert your precondition and make it behave like a type check. But then what happens if input doesn't meet the precondition? Do you throw an exception or crash?

I think that there should be a reference implementation for a useful static analyzer for preconditions, for it to be added to the language. Obviously it would be nice if you could verify that callers only pass in x > 5 to your function, but I think deferring the semantics for contracts to however the build/compiler chooses to handle them (because they might, one day) is not good enough for adding a new feature and syntax to a language. If preconditions can be used for useful static analysis beyond what static asserts and the type system gets you already, there should be evidence for that. I'm skeptical that you can do any better than a regular static assertion/type checks.

Also, I do think the lack of explicit handling (if in practice preconditions are only generally evaluable at runtime) in the contracts syntax is bad. The proposed syntax looks too much like a type or static assertion for a runtime check (note that you can easily see what CHECK/DCHECK macros actually do just by clicking through to their definition). And if it isn't in practice just a runtime check, there should be proof!