Skip to main content
17 votes
Accepted

How can all functions be total in Isabelle?

If you have a Isabelle/HOL function f :: a ⇒ b between two types a and b (NB: the function ...
Joachim Breitner's user avatar
7 votes

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,553
5 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,256

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