&gt; With dependent types, the line between tests and types becomes blurrier.<p>I came to the same realization a while back.  In principle, in a sufficiently expressive system one could encode any unit test as a type - although whether that could ever be <i>useful</i> is a separate question...