Re: [Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.

On 04/05/2010, at 13:30, Luke Palmer wrote:

On Mon, May 3, 2010 at 11:07 AM, Kyle Murphy wrote:

...

The fact that it doesn't is proof enough that there's a problem with it even if that problem is simply that the types you're using aren't exactly correct. Further, I'd argue that in the first instance with a non-strict type system, the instance of wrong code that compiles would be higher. The only argument to support non-strict typing would be if you could show that it takes less time to track down runtime bugs than it does to fix compile time type errors, and any such claim I'd be highly skeptical of.

Clearly. But many people believe in this methodology, and use test suites and code coverage instead of types. Indeed, such practices are essentially "empirical type checking", and they afford the advantage that their verification is much more expressive (however less reliable) than our static type system, because they may use arbitrary code to express their predicates.

I don't think it's a question of types vs. testing. Rather, it's types + testing vs. just testing. How is the latter more expressive than the former for defining properties of programs? Also, testing loses a lot of appeal once you start dealing with concurrent programs. Testing for "this program doesn't have race conditions" isn't exactly easy. You want as many static guarantees as possible. Roman