3 ms·
Homotopy Type Theory doesn't really contribute much to logic (it's basically just type theory with a few extra rules) or programming languages (computer-assiste
by dvt 7y ago
Homotopy Type Theory doesn't really contribute much to logic (it's basically just type theory with a few extra rules) or programming languages (computer-assisted proofs are easier in HoTT, but that's about it).
HoTT is a foundations of mathematics thing (think ZF/ZFC), so it's a bit weird to see it on the list. But it's kind of hot right now, so you see it just about everywhere.
- adamnemecek 7y agoIt connects logic, topology and type systems. How is this not a big deal? It's also computation friendly.
- dvt 7y agoLogic and type systems have been connected since Frege (he coined "functional" and "non-functional" types[1]). Computation friendly is interesting, but not really revolutionary. Topology I'm not an expert in so I can't comment. [1] On Function and Concept, 1891; http://fitelson.org/proseminar/frege_fac.pdf http://fitelson.org/proseminar/frege_fac.pdf
- fmap 7y ago> Homotopy Type Theory doesn't really contribute much to logic Of all the things in this list, this is the one you think is odd? The idea behind homotopy type theory is a groundbreaking connection between type theory and abstract homotopy theory (really, higher-category theory) and had far reaching consequences in both areas. For example, cubical type theory solves many problems with equality in type theory and it was only developed by understanding the homotopical models of type theory that were developed for HoTT. I could give more examples, but seriously, this alone is a major advance in logic.