It is and isn't. The type system will try to prove that a program will behave in some specific ways without needing to run the program. The "specific ways it b

It is and isn't. The type system will try to prove that a program will behave in some specific ways without needing to run the program. The "specific ways it behaves" is what I call "properties". Property based testing will run the program and check as it is running that it behaves in some specific ways. In the end, they both can be used to demonstrate that some properties of a program execution hold, but they go about it differently. The type system will use logic over the code semantics and structure to assert that in all possible cases (combination of inputs) the property will hold. The property based testing will use sampling to assert that in a lot of cases (combination of inputs), the property will hold. Unless you can sample the entire input range in a property based test, you don't prove that it holds for all inputs, just for a large number of them. While type systems tend to prove for all inputs. Also generally the type system will take less time to execute its reasoning over the code, than the property based test will take to run its sample set.