[userbinator]

I also would argue that the design of CPUs such that any sequence of bits could be loaded in any in any register and interpreted depending of the current context, instead of having typed registers is not a shortcoming but a fundamental feature. It makes code small and elegant.

Indeed, the fact that digital data is fundamentally "untyped" and its meaning depends entirely on interpretation is the entire reason why computers are so powerful and general-purpose.

[eli_gottlieb]

From a type-theoretic perspective, a language can be either logically consistent by means of strong normalization xor Turing-complete. The untyped lambda calculus is the smallest, most elegant functional language on the right half of that fork. It's also not strongly normalizing, so you can't prove theorems with it -- oh well!

[YellPika]

> From a type-theoretic perspective, a language can be either logically consistent by means of strong normalization xor Turing-complete.

This is a common misconception. A counter-example: take System F, add an `IO` monad, and add a function `fix : forall a. (a -> a) -> IO a` for general recursion. Our language is now Turing-complete, but remains consistent since any falsehoods produced by `fix` can't escape the `IO` type, e.g. you can prove `fix id : IO _|_`, but not `_|_`.

[eli_gottlieb]

Fair enough, and that's been one of the approaches to paraconsistency and inconsistency in modal logic, too. Of course, from a theorem-proving perspective, it's utterly useless, as with a proof-checker, at some point I need to escape the monadic container and get back into `Prop`.