[KMag]

> > Yes, I've looked at some of these projects before. And I certainly think it's a good idea to use automated tools to try to prove properties about programs.

> But I'm more excited about things like property testing than I am about things like strong type systems. And I'm wondering specifically what is the value they bring.

By "property checking" you mean theorem proving.

Static type checkers are theorem provers. More powerful type systems allow more interesting and less intuitive proofs to be written. Sometimes, the type checker is integral to the compiler and is required to run on every build, and sometimes it's an external tool.

In any case, if you're adding annotations to your source code in order for a theorem prover to statically prove certain runtime properties, those annotations constitute a static type system which is type-checked by your theorem prover.

Maybe you don't like even a subset of your theorem prover to run on every build, but if you're in favor of machine-checked proofs of program behavior, you're in favor of static typing.

[jsnathan]

Property testing [1] is about semantics, the same as regular testing, and it does not require code annotations. [Edit: It's more like "fuzzing" than "model checking".] Type systems on the other hand aren't usually powerful enough to capture semantics.

They allow you to say things like, this function takes in a list of Foo objects, and returns one Foo object. But they don't really let you express whether the object returned is or is not part of the original list, and if it is, that it was chosen according to the right mechanism. That's what tests are for.

Without being able to express the semantics of code, I don't see how you can trust it. There may not be any type mismatches, but there sure can be lots of bad logic in there.

[1]: http://hypothesis.works/articles/what-is-property-based-test...