3 ms·
The curry lambek howard isomorphism has been known for a while. Coq, the language that is used by the posted textbook is a dependently typed language and was re
by crimsonalucard 7y ago
The curry lambek howard isomorphism has been known for a while. Coq, the language that is used by the posted textbook is a dependently typed language and was released 30 years ago.
- 6gvONxR4sf7o 7y agoNobody builds web servers in Coq, but they do in Haskell, which I believe has some form dependent types coming. That's the kind of moving from niche languages to increasingly mainstream ones I mean. From there, maybe eventually it gets refined and even later properly mainstream. Sorta, but not precisely. But it's the kind of progress I see as encouraging for the future of formal methods in mainstream software development.