Type Systems Are Asserts

I started reading Coders at Work last week, and the interviews with Simon Peyton-Jones and Peter Norvig reaped an idea that doctest, contracts.coffee, and focco sowed and cultivated. What’s the idea? Type systems are nothing more than a formal implementation of a half-baked program proving system.

This is a slight over-generalization. I want to stress that I don’t think type systems are bad, whether static or dynamic. I’ve just suddenly realized that, should you extend a type system with tools to define pre- and post-variants and invariants, as well as performance or probability requirements, as some unit tests do, you end up with a very nice assertion mechanism that could replace all the different tools currently used in programming.

As a means of testing out this idea, I’ve started investigating the Lively Kernel and want to see what might happen should I add a contracts.coffee layer with a mechanism for validating the program upon saving changes to a script.