alt Hacker NewsWhat'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?
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?
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).