alt Hacker NewsMost 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.
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?