News for hackers. Stuff that matters.
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.

There are no comments on this comment yet.