Doesn't ADA have some method of checking if the input/output of a function is within bound? Can't remember if its a runtime or compile check however.

But the concept of function contract verification would be interesting.