[quamserena]

Most existing mainstream languages aren’t expressive enough to encode these invariants. For languages outside of the mainstream, Lean 4 is a language supporting verification, and it’s also a full programming language, so you can write your proofs/theorems in the same language that you program in.

[fooker]

What's an invariant you can not encode in a general purpose programming language?

I'd have assumed, by virtue of being Turing complete, you could express any invariant in almost any language?

[wavemode]

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).