How would you ensure that the values of the types doesn't invalidate the contract? Easy for basic assignment, but not sure how you would do that when doing arbitrary mutation.
For operations/mutations where it's more complex to validate the inputs, you could assign the result to an unbounded variable, and then prove to the type checker that you're exhaustively handling the output before you assign it to a bounded variable. For example, multiply two unbounded numbers, store the result in an unbounded variable, then do "if result >= 1 && result <= 100 then assign result to var[1..100] else .... end"