4 ms·
Total layman here, but I thought one of the areas of significance is that a language that uses it can write code that is guaranteed to be bug-free, since the ty
by tunesmith 13y ago
Total layman here, but I thought one of the areas of significance is that a language that uses it can write code that is guaranteed to be bug-free, since the type system is rich enough to be able to prove correctness (given the problem being correctly stated).
- tel 13y agoThat has more to do with type theory directly. So far the lectures have been a great intro to constructive logics which while build to type theory and dependently typed languages, but that's not necessarily the thrust of HoTT.
- mafribe 13y agoBug-free is a bit strong, since you can only use a dependent type-theory like HoTT to establish that a program meets its specification, but the specification might be buggy.