[derdi]

I was confused by the matrix multiply example since it doesn't show requires clauses. So I looked at what is presumably the source I'm supposed to look at: https://github.com/bneb/lattice/blob/main/basalt/src/kernels...

There's a comment saying every function in that file has requires clauses, but... They don't?

Also, the actual implementation of matrix multiply is manually tiled, while the website boasts about automatic loop tiling. It's hard to know what to trust here.

[bneb-dev]

Looking. I did a huge purge/rewrite of the benchmarks and this might have regressed. Happy to track here or GitHub.

[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.