Jak je v IT všeobecně známo, typové systémy žijí dvojím životem. Na jednu stranu se tváří jako množiny a operaci nad nimi jako běžné programy, ale na stranu druhou odpovídají typy logickým tvrzením a jejich prvky důkazům. Příslušná symbolická logika není ovšem logikou známou z matematiky. Jde o tzv. logiku intuicionistickou, ve které mnohá tvrzení považovaná za samozřejmá neplatí.