Rust's type system is Turing-complete (2017)

I think we should strive for strong type systems with a lot of type inference. I especially like Typescript for that.

Type systems are very useful to establish the semantics of your operations. For example `int + int` is not the same operation as `string + string`, and definitely not the same as `int + string` (which does not exist in most languages). You could call `+` an addition, but addition only exists for numbers, for strings it is a concatenation.

Is `int + string` the same as `string + int` ? (commutativity)

Is `int + int + string` the same as `(int + int) + string` or `int + (int + string)`? In that case, what does `int + string` returns? (associativity)

Now consider this code:

  def foo(a, b):
    return a + b

vs

  function foo(a: int, b: string) {
    return a + b
  }

In the second case, your function obviously seems wrong.

Finally, in math an object does not "have a type" but "belongs to a set/class". For example, "1" is an integer, an odd number, a real, a complex, a scalar, a rank 1 tensor, etc... Saying that "1" is only an integer is incorrect, but that's what most programming language do.

I've tried to design a language where "typeof variable == type" does not exist but instead you have "variable isof type" running the type checking code, example:

  class user(v: struct {
    name: string,
    logged_in: bool
  })

  class logged_user(u: user) check
    # this code is evaluated when 'isof' is called
    u.logged_in = true
  end

  class allowed_user(u: user) check
    # =>,  operators are logical connectors
    # A => B is true if A and B are true or A is false
    # A  B is true if A and B are both true
    u isof logged_in  u.name in ['admin', 'root']
  end

  let alice = { name: 'alice', logged_in: false }
  assert alice isof user = true
  assert alice isof logged_user = false
  assert alice isof allowed_user = false

  let bob = { name: 'bob', logged_in: true }
  assert bob isof user = true
  assert bob isof logged_user = true
  assert bob isof allowed_user = false

But lazyness got the best of me and I only implemented the parser :(

> Most if not all Turing-complete systems are also known to be Turing-equivalent. (I regret not being able to find a better citation for this.)

It links to Wikipedia (WP), which defines "system" by:

> a computational system (such as an abstract machine or programming language)

there is no better citation[0], because it's not true under some definitions of "computational system", per WP's definition of "computational system" [3]. For example, under the WP definition of "abstract machine", a non-computable function satisfies the definition. Or we can define it as follows: input: strings in an alphabet A, output: {true, false}, operations allowed: check for membership in a language L in alphabet A.

So we see that theoretical formal languages are a subset of computational systems. But there are uncountably many formal languages and only countably many TM. Crucially, we can easily turn each language into one that acts as a universal turing machine while still being distinct. Hence there are uncountably many Turing-complete languages for a given alphabet A[2]

[0]: incidentally, the linked WP page claims slightly differently (unimportantly) that "All known Turing-complete systems are Turing-equivalent, which adds support to the Church–Turing thesis."

[1]: "A typical abstract machine consists of a definition in terms of input, output, and the set of allowable operations used to turn the former into the latter." Absent a more precise definition, I assume the set may include arbitrary mathematical operations (and it is useful to define non-computable abstract machines, and in general usage in the field abstract machines may refer to languages more powerful than Turing machines).

[2]: Sketch: Let U' be a Universal TM in alphabet A (hence U is Turing-complete), let M' denote the language it accepts, and let 0 be a symbol of A. Define M such that if i' in M', then i in M, where i is i' with every symbol duplicated and 0 prefixed (hence if i'="123", i="0112233") Define N such that if i' in complement(M'), then i in N, where i is i' with every symbol duplicated and 0 prefixed. Observe that every language disjoint from N that contains M is Turing-complete (wrt a slightly modified description for TMs and the simulated input than the one for U'). Now, let L be an arbitrary language in A. Define f(L) = { j | j' in L, j is j' with every symbol duplicated }. Then we see that f(L), M, N are all disjoint. And if T, U are distinct languages, so (f(T) union M) and (f(U) union M) are distinct languages that simulate Turing machines (i.e. they are Turing-complete). Hence there are uncountably many Turing-complete languages. There are only countably many Turing machines, hence only countably many Turing-equivalent languages, so in fact most Turing-complete languages are not Turing-equivalent languages.

[3]: of course,

I personally found Go far more unproductive than Python - doing if err!=nil a zillion times and writing the nth for loop..it made me cry worse than cutting fresh onions.

Python is not Perfect (bad general-purpose performance), but IMHO honestly a more productive language than Go.

And Python has type hinting nowadays which is sweet when you want it. Type hinting is good for self-documenting stable code.

This isn't a problem at all for modern type systems. OCaml, Haskell, and even C++ have Turing complete type systems and this is one of the last concerns for developers.

The article is fascinating and I love fun stuff like this, but the discussion is a bit off the rails. There are a lot of things that are accidentally Turing complete. Turing complete is not synonymous with complicated and unwieldy to use. I mean, okay, maybe if you are doing the stuff that the author is doing it is complicated and unwieldy - in fact to the point that you would never do it in the first place. But Turing completeness is really not a high bar to reach.