Re: Axiom musings ... runtime computation of first-class dependent types

Martin, >In this series of videos Robert Harper gives an provocative take on >these subjects: >https://www.youtube.com/watch?v=LE0SSLizYUI I watched Harper's videos years ago. I will revisit them. If you haven't seen them I highly recommend them.

Re: Axiom musings ... runtime computation of first-class dependent types

Tim In this series of videos Robert Harper gives an provocative take on these subjects: https://www.youtube.com/watch?v=LE0SSLizYUI At about 37 min into this video he says: "what is true has unbounded quantifier complexity whereas any formalism is always relentlessly recursively

Axiom musings ... runtime computation of first-class dependent types

Well, SANE is certainly turning into a journey. When we look at the idea of first-class dependent types as implemented in languages like Agda and Idris we find what I call "peano types". For example, Fin is a type of "finite numbers", usually defined as data Fin : Nat -> Type where FZ : Fin (S