3 ms·
This is an explicit goal of one of of the creators of homotopy type theory, Fields medalist Vladimir Voevodksy: https://www.ias.edu/ideas/2014/voevodsky-origins
by jkhdigital 5y ago
This is an explicit goal of one of of the creators of homotopy type theory, Fields medalist Vladimir Voevodksy: https://www.ias.edu/ideas/2014/voevodsky-origins https://www.ias.edu/ideas/2014/voevodsky-origins
Apparently he now uses Coq in his everyday work.
- alexilliamson 5y agoHe's been dead for four years?
- dhosek 5y agoApparently he didn’t shut down his computer before he died.
- queuebert 5y agoDat uptime tho
- jkhdigital 5y agoOh snap, I had no idea that he died! Wow... that's a profound loss for the field of mathematics.