In most languages you can express any invariant, sure, but you can't prove that the invariant is upheld unless you run the program.

For example a NonNegativeInteger type in most languages would just have a constructor that raises an exception if provided with a negative number. But in languages with proofs, the compiler can prevent you from constructing values of this type at all unless you have a corresponding proof that the value can't be negative (for example, the value is a result of squaring a real number).