3 ms·

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 i

• wavemode 11mo ago
  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).