Comment by lenkite

spec is mostly useless for tools and IDE's and static analysis. Spec necessitates running your program with an arbitrary runtime complexity. Type checking is done before your program runs. The idea is to remove the need for runtime checks as much as possible.