Adding to your point, spec goes beyond the power of a (garden variety) type system, since it does its work at runtime. This of course incurs a performance hit,

Adding to your point, spec goes beyond the power of a (garden variety) type system, since it does its work at runtime. This of course incurs a performance hit, but you can easily exclude these checks in a prod build just by setting a compiler flag.