(N.B. The word “fuck” appears multiple times in this post. I recommend that the reader temporarily not consider “fuck” as profanity, as it isn’t used that way here.)
Not so long ago, a certain someone made a challenge on the Rust subreddit asserting that while everyone likes to say that Rust’s type system is Turing-complete, no one actually seems to have a proof anywhere. In response to that post, I constructed a proof in the form of an implementation of Smallfuck – a known Turing-complete language – entirely in the Rust type system. This blog post is an attempt to explain the inner workings of that Smallfuck implementation, as while as what this means for the Rust type system.
So what is Turing-completeness? Turing-completeness is a property of most programming languages which states that they can simulate a universal Turing machine. A related notion is Turing-equivalence. Turing-equivalent languages can simulate and be simulated by Turing-machines – so if you have any two Turing-equivalent languages, it must be possible to translate any program written for one into a program written for the other. 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.)
There are several important things to note about Turing-completeness. We know about the halting problem. One consequence of this is that if you have a Turing-complete language, which can simulate any universal Turing machine, then it must be capable of infinite loops. This is why it’s useful to know whether or not Rust’s type system is Turing-complete – what that means is, if you’re able to encode a Turing-complete language into Rust’s type system, then the process of checking a Rust program to ensure that it is well-typed must be undecidable. The typechecker must be capable of infinite loops.
How do we show that the Rust type system is Turing-complete? The most straightforward way to do so (and in fact I don’t know of any other ways) is to implement a known Turing-complete language in it. If you can implement a Turing-complete language in another language, then you can clearly simulate any universal Turing machine in it – by simulating it in the embedded language.
So, what’s Smallfuck? Smallfuck is a minimalist programming language which is known to be Turing-complete when memory restrictions are lifted. I chose it to implement in the Rust type system over other Turing-complete languages because of its simplicity. While esoteric languages are fairly useless for actually writing programs, they’re great for proving Turing-completeness.
Smallfuck is actually pretty close to a Turing machine itself. The original specification for Smallfuck states that it runs in a machine with a finite amount of memory. However, if we lift that restriction and allow it to access a theoretically infinite array of memory, then Smallfuck becomes Turing-complete. So here, we consider a variation of Smallfuck with infinite memory. The Smallfuck machine consists of an infinite tape of memory consisting of “cells” containing bits along with a pointer into that array of cells.
Pointer |
v
...000001000111000001000001111...
Smallfuck programs are strings of five instructions:
< | Pointer decrement
> | Pointer increment
* | Flip current bit
[ | If current bit is 0, jump to the matching ]; else, go to the next instruction
] | Jump back to the matching [ instruction
This gives you the ability to select cells and make loops. Here’s a simple example program:
>*>*>*[*<]
This is a dead simple and totally useless program (as most programs are in Smallfuck, thanks to its total lack of any sort of I/O whatsoever) which simply sets three bits in a row to 1, and then uses a loop to put them all back to 0, ending with the pointer in the same location it started. A visualization:
Instruction pointer
| Memory pointer
v v
>*>*>*[*<] | ...0...
The first instruction moves the pointer to the right. All cells default to 0:
v v
>*>*>*[*<] | ...00...
The next instruction is a “flip current bit” instruction, so we flip the bit at the pointer from 0 to 1.
v v
>*>*>*[*<] | ...01...
This occurs three times. Let’s skip ahead to the start of the loop: