> The issue with bound checks for exemple is entirely avoidable if you prove that all your calls are within bounds before compiling, same thing for partial initialization.
The situation is more nuanced. The article dedicates a section to it:
> The general idea in eliding unnecessary bounds checks was that we needed to expose as much information about indices and slice bounds to the compiler as possible. We found many cases where we knew, from global context, that indices were guaranteed to be in range, but the compiler could not infer this only from local information (even with inlining). Most of our effort to elide bounds checks went into exposing additional context to buffer accesses.
I think the comment you replied to is about a different approach: writing the algorithm in assembly or C, and then proving it doesn't access anything out of bounds.
This is the WUFFS approach, for example. Formal verification, while very cool, is extremely tedious, which is why more practical languages try to find compromise rules that are simpler to implement, while also not too limiting.
The situation is more nuanced. The article dedicates a section to it:
> The general idea in eliding unnecessary bounds checks was that we needed to expose as much information about indices and slice bounds to the compiler as possible. We found many cases where we knew, from global context, that indices were guaranteed to be in range, but the compiler could not infer this only from local information (even with inlining). Most of our effort to elide bounds checks went into exposing additional context to buffer accesses.
(extensive information given in that section)