Hacker News Reader

Thanks! Interesting. I'll try to dig out the recent papers. Although I have a feeling that most of this is not that new. LLVM is just a very basic SSA, which is early 90s. Agda builds on similar grounds as things like Coq, Minlog, even ACL2 and Isabelle, which are very old. There've been a lot of buzz in the concurrent code verification ever since the early pi-calculus papers by R. Milner.

But the liquid type inference seems to be a genuinely new thing, and apparently I totally missed it somehow. It even seems like I unknowingly reinvented something similar, by using arbitrary Prolog code as type attributes on top of a basic Hindley-Milner.

Agda builds on similar grounds as things like Coq, Minlog, even ACL2 and Isabelle, which are very old.

… Coq, Minlog, even ACL2 and Isabelle build on similar grounds as Chrysippus’ in the 3rd century BC …

i.e. there’s nothing new under the sun.

Dependent types, gradual typing, HoTT

HoTT?