Skip to main content
8 votes
Accepted

Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

[Supplemental: I rewrote the answer so that any shred of vagueness is gone, as it was evoking religuous zeal, and I would prefer to stick to math. Everything is explained in terms of a widely accepted ...
Andrej Bauer's user avatar
  • 9,802
6 votes

Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

Is this perhaps a problem with 'common understanding' regarding what it means to be Turing complete? Indeed it is: a pop-science understanding of dependent types has led to this myth being deeply ...
gallais's user avatar
  • 1,266
3 votes

Implementability of proof assistants for Infinitary logics with finite many terms

I don't think this question is well formed for the following reasons. As stated in the answer to a similar math stack exchange question, there are uncountable many $\mathcal{L}_{\omega_1, \omega}$ ...
Jason Rute's user avatar
  • 9,195

Only top scored, non community-wiki answers of a minimum length are eligible