There are some languages heading towards this. ATS [1] provides a restricted form of dependent types [2] that allows you to do what you want and is designed for

There are some languages heading towards this. ATS [1] provides a restricted form of dependent types [2] that allows you to do what you want and is designed for systems programming. You can do safe pointer arithmetic for example. Idris [3] is another language with dependent types (and is more Rust-like) designed for systems programming. I don't think Idris has type level presberger arithmetic though making some things a bit verbose. [1] http://www.ats-lang.org/ http://www.ats-lang.org/ [2] http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.html http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.h... [3] http://www.idris-lang.org/ http://www.idris-lang.org/