2 ms·
> With dependent types, the line between tests and types becomes blurrier. I came to the same realization a while back. In principle, in a sufficiently expres
by dllthomas 11y ago
> With dependent types, the line between tests and types becomes blurrier.
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 useful is a separate question...
- adamnemecek 11y agoThis way one of my takeaways from Curry Howard isomorphism.
- js8 11y agoExactly. Well, mathematicians do that, they encode everything in the type, which they call the theorem or lemma (while the program itself is the proof). But mathematicians, it seems to me, tend to do a lot of proof copy-pasting, unless they use category theory or something like that.