> "Types" is just one form of, in many languages quite limited, specs. That's the "Curry types" perspective described in the article, yes. "Church types" are s

> "Types" is just one form of, in many languages quite limited, specs. That's the "Curry types" perspective described in the article, yes. "Church types" are syntax, not specification. In Haskell, for example main = print (5 + "foo") isn't a program that fails to conform to its spec, it's just not a program. It has no meaning and no behavior, not wrong behavior. You can (but should never) `unsafeCoerce` `5` to `String` or `"foo"` to `Int` and get something broken out - but they'll be different broken things, and neither will in any sense be the compiled form of the `main` function above.