I think the correct solution is for the type system to be able to say "Hey, this unsigned int is being subtracted from and was not checked to ensure it is great

I think the correct solution is for the type system to be able to say "Hey, this unsigned int is being subtracted from and was not checked to ensure it is greater than the value being subtracted." And the typical solution would be to either a) invert the subtraction to an addition, b) do a check, or c) annotate the type.