> The article makes no mention of this, so in the context of the article the title remains very wrong

The temp allocator implementation isn't guaranteed to detect it, and the article doesn't go into implementation details and guarantees (which is good, because capabilities will be added on the road to 1.0).

> I tries searching how these contracts work in the C3 website [1] and these seems to be no guaranteed static checking of such contracts.

No, there is no guarantee at the language level because doing so would make a conforming implementation of the compiler harder than it needs to be. In addition, setting exact limits may hamper innovation of compilers that wish to add more analysis but will hesitate to reject code that can be statically know to violate contracts.

At higher optimizations, the compiler is allowed to assume that the contracts evaluate to true. This means that code like `assert(i == 1); if (i != 1) return false;` can be reduced to a no-op.

So the danger here is then if you rely on the function giving you a valid result even if the indata is not one that the function should work with.

And yes, it will be optional to have those "assumes" inserted.

Already today in current compiler, doing something trivial like writing `foo(0)` to a function that requires that the parameter > 1 is caught at compile time. And it's not doing any real analysis yet, but it will definitely happen.

Just my opinion, but I think that having contracts that might be checked is a really really really dangerous approach. I think it is a much better idea to start with a plan for what sorts of things you can check soundly and only do those. "Well we missed that one because we only have intraprocedural constant propagation" is not going to be the sort of thing most users understand and will catch people by surprise.

Well, we've already tried that, and no one used it.

Safety is a spectrum. You add +1 and safety goes up.

> The temp allocator implementation isn't guaranteed to detect it, and the article doesn't go into implementation details and guarantees

Understandable, but then why are you mentioning the borrow checker if you avoided mentioning _anything_ that could be compared to it.

> No, there is no guarantee at the language level

Then don't go around claiming they are statically checked, that's false. What you have is a basic linter, not a statically enforced contract system.

Oof that sounds incredibly dangerous and basically means it doesn't really offer much of an improvement over C imo in terms of safety.

What is "incredibly dangerous"? Having contracts that can catch errors at compile time?

I understood your comment as that contracts are not statically checked at compile time. That is incredibly dangerous and means I would never go to bat for the language.