Comment by derdi

For here (and the website), I would be more interested in trustworthy information about what is actually verified at compile time, and what happens when verification fails.

What if you write a function that takes an array (as an array type if you have one, or as a pointer, or a slice, or whatever). It returns `array[0] + array[1]`, but it has no bounds checks in the code, neither as actual `if` statements nor as `requires` clauses.

Verification of such a function must fail at compile time, right? Does it? What does the error message look like? Someone else found some quote somewhere that seems to suggest that integer overflow checks are implemented as runtime checks if you can't eliminate them at compile time. Does that also happen for bounds checks? If yes, does the user get a warning saying that M out of N checks were moved to run time?

It's just really unclear if you are really doing "Verified safety without the runtime cost." or if you have reinvented Java, which will be just as good (actually better) at eliminating these bounds checks as compile time.