[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...