~yosh@unix.dog

turing complete until it isn't

posted

modified

This post is going to be a bit of a ramble, as it’s a written form of a conversation I had in voice chat with a friend, stemming from a different topic we were talking about as opposed to planned out writing. The context was discussion of programming languages like koka and ATS that allow you to track more things at compile-time (such as side effects of a function or dependent types) and thus prevent certain kinds of soundness bugs that may occur in less tracked languages.

I was thinking about the term “turing completeness” and what it like, really means. I didn’t exactly get an “academic” look into the theory of computation during my education, so the most insight I ever got into that side was a description of Rice’s theorem at one point.1 Like, obviously, I had an idea of what “turing complete” means, usually cobbled from internet browsing, but I never looked at it closely. As a sanity check, I first just looked at Wikipedia, where it describes that a “system of data manipulation rules…is said to be turing complete…if it can be used to simulate any Turing machine”.

Which, well, yeah. Duh. It’s what I thought. But like, any turing machine? On a flat plane of memory? It got to this point where they went to do something else for a bit, and I was left pondering my own thoughts. My mind drifted to Rust and its borrow checker. The borrow checker restricts the set of programs you’re allowed to write, and in safe rust, you can’t manually modify, say, length of array references or whatnot… does this mean that Rust is not turing complete, since there are turing machines that would violate Rust’s borrow checker rules?

Obviously not, I quickly realized. You can just, not use any of those features. Allocate a large array of integers, run brainfuck on it, and there’s your turing completeness. You’re able to allocate said array anywhere and of any size, so memory is theoretically unrestricted—you can access any address—and any computation can be made.2 So it’s not inherent to Rust The Language itself. Where does that line emerge?

Oh, you don’t even need to look at the borrow checker. If you instantiate an enum in Rust (or a sum type in any other language—there’s no need to only look at Rust now), the tag that holds what variant the instantiated enum object is must exist somewhere in memory. For simplicity, I’ll just say it’s some integer at some address. The constructs of the language will then not allow you, barring compiler bugs, to write an integer to the tag address that does not correspond to a valid enum type. So, in essence, the set of possible programs that are able to be constructed in the language after you have instantiated a sum type is no longer turing complete, as any turing-like machine that writes to the address of the sum type’s tag is no longer representable after that point. This is in contrast to say, C, where enums there do not have that type safety. You can write any value to an enum at any time, and the set of representable programs does not decrease in size after instantiating an enum type.

Again, this isn’t a very academic and formal look at it. I don’t know if what I said is followable as a strict line of logic. But it intuitively feels sane to me, knowing that typed computational constructs like the simply typed lambda calculus are not turing complete.3 It was an interesting thread to follow, though, and I think it helped me internalize how fickle terms are compared to real world applications. You can compute anything in any language, but once you introduce a strict construct of the language into your program, you may no longer be able to compute anything after that point. Typing restrictions and tracking things allow for more invariants to be known—you’ll know, for a fact, that the tag of an enum will not be invalid during the lifetime of a program. That’s provable at compile time! That’s going against Rice’s theorem because the set of programs has provably decreased from “turing complete” to “almost turing complete except the machines that write to that address”!

does mainstream programming culture know this?

When thinking back on this and writing it down, it seems like such an obvious statement. Hell, even the Wikipedia page for Rice’s theorem describes how type systems begin to make previously undecidable properties of a program decidable. If it’s so obvious, though, why aren’t languages with effects like koka, or dependent types like ATS, much more popular? Why haven’t they taken everything over, since we’re able to prove more things at compile time? What gives?

Remember how I said that the most I was ever told of the theory of computing during education was just a description of Rice’s theorem in a random class? This seems to be a general experience among North American universities, where “computer science”, at least during undergraduate years, is more focused on the trade of computer science as opposed to the formal side unless you go to a very specialized research university.4 In my formal education, I was only ever introduced to C-like languages for program development.5 These languages aren’t exactly known to have extensive and robust annotations for anything other than basic type checking.

This is how it’s been for a while. Education has focused on “industry” languages, all mostly C-like, and have passing, surface-level mentions of theory that get locked in the mind as aphorisms without deeper thought. If all the insight you ever get in this domain is your first-semester computer science professor exclaiming how exciting computers are, a mysterious comment on how “you can’t prove if a program halts or not”, and all languages you use imbue that, it’s not out of the question that it just sticks with you endlessly. Stuff like this is hard to break for people. I frequently find myself huffing and puffing when I see users of mainly C-like “mainstream” languages unaware of exotic, unique, and wonderful programming languages that break a lot of conventional ideas people have about programming.

So, I guess the lament is the same as always: PL theory isn’t a known area that much, and industry is stuck with the same languages they’ve been using for the past X years. Rust is probably the only language with these kinds of “turing restrictions” that has gotten attention from “mainstream programming culture”, and even then it’s flaky. It’s awesome that a language with that kind of checking, where you can write any (safe) Rust code and guarantee that you’ll never have memory soundness bugs, has gotten attention, but the attention has only been focused on the results of that endeavor (memory safety), and not of what could happen if you took the kind of tracking Rust does to other classes of soundness bugs.

This entire conversation and thought process stemmed from a dev comment on a UGC platform’s bug tracker stating that guaranteeing sound conflict resolution of duplicated data from arbitrary user code was impossible. It certainly is impossible if the “arbitrary user code” is written in about any existing programming language right now, but it’s not impossible to devise a language that guarantees a correct replicated data conflict management type. It’s just not something that people think can be tracked in the first place, because basically no language right now does.

That’s all. Hopefully this was at least kind of followable. I am not good at closings. Farewell.

  1. The only class I took that ever mentioned Rice’s theorem was one about reverse engineering malware. No other required or elective class in my degree mentioned it. ↩︎

  2. I feel like if I don’t mention that I’m aware it’s not technically fully turing complete since memory is finite, I’ll have ten million people e-mailing me about it. You guys know what I mean. Be reasonable. ↩︎

  3. The simply typed lambda calculus is not turing complete as you can’t represent recursion in it, which is a different blocker than what I described, but it’s the general idea of “imposing typing restrictions is known to maybe halt turing completeness” that I connected with in my mind. ↩︎

  4. I’m curious to see if there’s a general difference between the US and Europe on CS education. I definitely do not have a complete perspective, but I want to say that my limited observations of European education makes me feel like theory is emphasized a bit more than it is here. But again, I do not know for sure. ↩︎

  5. I did use VHDL for hardware design, which was the only class-wide taste at different paradigms of programming. I compared functional programming to VHDL’s “combinatory” programming initially, since both are declarative in nature. I also had a brief encounter with Elixir for one assignment in a class where the overall project was making an interpreter for a toy language. ↩︎

back