Agreed in general, but it is possible to enable this style of constraint propagation by being restrictive about what kind of contraints you can write. In particular, the "LIQUID" family of languanges that have been developed at UCSD allows properties which are conjunctions of LInear IneQUlites, and can infer them automatically. The programmer would annotate one declaration of a variable with a constraint like (0 <= x < 10), and the system tries to infer suitable constraints for all other variables (calling out to an SMT solver, and using invariant inference techniques from the program analysis community).

Their latest research language is "Liquid Haskell", I think it could deal with jarrett's example out of the box (with the caveat that yes, you still need to write the test explicitly). They used to have an online demo where you could just type programs into a web form, but that doesn't seem to work right now...