Comment by vrighter

not of the implementation. Of the type system. And a verification of subsets, but not a verification of their interactions == the whole system is unverified.