>> Consider a program in which an array was accessed based on the index provided by some user input -- how could this ever be proven to never go out of bounds?
> It's a type constraint on the index
Consider a program in which the index type is provided by some user input -- how could this ever be proven to never go out of bounds?
You can move the problem elsewhere (and indeed often should!), but eventually it becomes a condition check and error handling behavior appropriate to the scenario. The default error handling behavior is to halt the program.
> It's a type constraint on the index
Consider a program in which the index type is provided by some user input -- how could this ever be proven to never go out of bounds?
You can move the problem elsewhere (and indeed often should!), but eventually it becomes a condition check and error handling behavior appropriate to the scenario. The default error handling behavior is to halt the program.