I bring up the lack of turing completeness because in the space of type languages you can make even more powerful arguments. What you mention about reasonable encodings is sufficient, but we can get more strength.
And, yeah... even a type system as primitive as C can catch interesting invariants. This is an important counterpoint to the general idea that "types never say anything interesting".
"I bring up the lack of turing completeness because in the space of type languages you can make even more powerful arguments. What you mention about reasonable encodings is sufficient, but we can get more strength."
Certainly. I had every confidence you understood that. I just wanted to be sure we avoided strengthening the "Turing complete means it can do anything any other language can" misconception.
And, yeah... even a type system as primitive as C can catch interesting invariants. This is an important counterpoint to the general idea that "types never say anything interesting".