> Usually the "foundation" is taken to be some kind of type theory … which has some … limitations (e.g. languages cannot be Turing complete) that I don't really

> Usually the "foundation" is taken to be some kind of type theory … which has some … limitations (e.g. languages cannot be Turing complete) that I don't really understand … One sentence summary that glosses over a lot of things: In a dependently typed language, types can contain programs, and we want typechecking to terminate. You may also want to read how the author of Idris explains partial and total functions: https://livebook.manning.com/#!/book/type-driven-development-with-idris/chapter-1/141 https://livebook.manning.com/#!/book/type-driven-development...