Taken literally the claim isn’t true - a Turing complete type system can enforce any constraint that a Turing complete programming language can. But your everyday type systems typically can’t express concepts like “a list of at least 3 elements” or “a number which is a power of 2”.
Pardon my ignorance, but can this spec thing automatically deduce that 8^n evaluates to "a number which is a power of 2" or log(2, "a number which is a power of 2") is an integer?
If yes, then I agree this is super helpful (and magical).
If not, how is this different from a normal constrcutor (with runtime input validation)?
No, it's not automatic like that. You define predicate functions that need to evaluate to true to pass. One of the reasons this is better than a normal constructor is these predicate functions are attached outside of the function they're describing. So they're inspectable and composable.
