Two asides, which I don't think you missed but I just wanted to expand on...
First, "Turing complete" means that you can compute anything anyone else can compute. It doesn't necessarily mean you can do it with a reasonable encoding, or do with it what you need to do with it. At the boundary between systems, encoding matters quite a lot!
Second, it's certainly true that there are constraints you can express in Haskell and not in C, but I was surprised by some of the things I could enforce in C with a little creativity.
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.
First, "Turing complete" means that you can compute anything anyone else can compute. It doesn't necessarily mean you can do it with a reasonable encoding, or do with it what you need to do with it. At the boundary between systems, encoding matters quite a lot!
Second, it's certainly true that there are constraints you can express in Haskell and not in C, but I was surprised by some of the things I could enforce in C with a little creativity.