3 ms·
They are, and that is one of the nice things of a type system like this. (I believe that's the "dependent types" bit.) It lets you express quite powerful theore
by tomsmeding 8y ago
They are, and that is one of the nice things of a type system like this. (I believe that's the "dependent types" bit.) It lets you express quite powerful theorems about (simple?) programs without having to stray too far from the language.