Dependent C-style types with subtyping rule
I think the best setup here is Liquid Types, but compared to the original Liquid Types paper, you would want a much weaker language of constraints. Also, if you don't need type inference, it's even easier. 

You'd still have to solve linear programs, though. Consider this function:

{int | (&lt; 30) /\ (&gt;= 10)} foo({int | (&gt; 20)} bar, {int | (&lt;= 70)} baz) {...} 


and you do some arithmetic on bar and baz inside the function. Then, to type check the function, you'd have to make sure that this expression takes a value between 10 and 29, which means you'd still need to solve linear programming (treating all non-constant multiplication as atoms), which is NP-complete. However, it is known that linear programming can be polynomial if you fix the number of variables involved. What implications do this fact have on our system? I don't really know as I'm not an expert in this area.

But I suspect what you really want is some sort of symbolic execution or abstract interpretation. If your language is completely first-order and doesn't have pointers, both should be pretty easy, and would involve far less human work (i.e. type annotations).