[kevlar700]

Ada is very flexible and does let you leave out the runtime check. However the program will be stopped or atleast be exceptive by default if a logic error creates an invalid value that you haven't checked the validity of. Spark can be used for a higher degree of value analysis at compile time because flow analysis is obviously needed in many cases. Volatility can still be an issue but in most cases Ada knows the inputs such as for API usage validity.

[samatman]

I would rather say that Ada allows you to remove the runtime check on ranges. This is the opposite of enforcing a range with a home-rolled check of the values, that's what I mean by "won't let you leave it out": without deliberate action, the range will either be proven by static analysis to be in-bounds, or that invariant will be checked at runtime.

Julia has a similar system for array bounds: by default, accessing an array is checked for range restriction, and an error is thrown if the value is out of range. Range checks inside functions (including the system `getindex` function) can be annotated with the @boundscheck macro, and user code which knows an index is in-range can use @inbounds to elide that check. If this is done wrong, Julia will segfault or corrupt memory. In C, if it isn't all done perfectly correctly, same thing: opt-in, not opt-out. Julia is more like Ada in that respect.