Re:Show HN: Dependently typed language for proofs that you c...
by caotic123 on Sunday October 03, 2021 @04:23PM
(#28740228)
The simplicity comes from picking simple abstractions to build a dependent type checker. If I have decided to put linear types in PomPom, for example, you will probably waste more time implementing it than actually capturing a lot of expressivity. So the point is to pick what you think is better in the trade-off.
[ Parent
| on HN ]
There are no comments on this comment yet.