Not inexpressible. Unprovable. There could be a set of correct programs that could never be proven correct by a type checker, for example.