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

[Roman Leshchinskiy]

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

> On Mon, May 3, 2010 at 11:07 AM, Kyle Murphy <orclev at gmail.com> 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